add — Mathlib

English

The zero matrix represents the zero endomorphism in the special case shown.

Русский

Нулевая матрица представляет нулевое отображение в указанном случае.

LaTeX

$$$(0:\\ Matrix ι ι R)\\ Represents b 0$$$

Lean4

theorem add {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 at h h' ⊢; rw [map_add, map_add, h, h']

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