mul — Mathlib

English

If A represents f and A′ represents f′, then the product A A′ represents the product f f′ with respect to the same basis b.

Русский

Если A представляет f и A′ представляет f′, то произведение A A′ представляет произведение f f′ по той же базе b.

LaTeX

$$Matrix.Represents b A f → Matrix.Represents b A' f' → Matrix.Represents b (A∘A') (f∘f')$$

Lean4

theorem mul {A A' : Matrix ι ι R} {f f' : Module.End R M} (h : A.Represents b f) (h' : Matrix.Represents b A' f') :
    (A * A').Represents b (f * f') :=
  by
  delta Matrix.Represents PiToModule.fromMatrix
  rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_mul]
  ext
  dsimp [PiToModule.fromEnd]
  rw [← h'.congr_fun, ← h.congr_fun]
  rfl

Похожие утверждения