Theorems · Theorem · linear algebra

Matrix.Represents.congr_fun

∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f : Module.End R M},
  Matrix.Represents b A f →
    ∀ (x : ι → R), (Fintype.linearCombination R b) (A.mulVec x) = f ((Fintype.linearCombination R b) x)

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Cited by

2 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeAddCommGroupCommRingModuleDecidableEq