eq — Mathlib · SciLib

English

Equality of representations is preserved under addition of matrices and endomorphisms.

Русский

Равенство представлений сохраняется при суммировании матриц и эндоморфизмов.

LaTeX

$$Matrix.Represents b A f → Matrix.Represents b B g → (A+B).Represents b (f+g)$$

Lean4

theorem eq (hb : Submodule.span R (Set.range b) = ⊤) {A : Matrix ι ι R} {f f' : Module.End R M} (h : A.Represents b f)
    (h' : A.Represents b f') : f = f' :=
  PiToModule.fromEnd_injective R b hb (h.symm.trans h')

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