Theorems · Theorem · linear algebra

AlgEquiv.mapMatrix_apply

∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Algebra R α] [inst_6 : Algebra R β]
  (f : α ≃ₐ[R] β) (M : Matrix m m α), f.mapMatrix M = M.map ⇑f

Defined in: Mathlib.Data.Matrix.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq CommSemiring Semiring Semiring Algebra Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
AlgEquivstatement and proof · cited by 1,681
Matrix.mapstatement · cited by 247
AlgEquiv.mapMatrixstatement and proof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

Matrix.reverse_charpolyproof · cited by 3