baseChange_sub — Mathlib

English

Base-change respects addition of linear maps: baseChange_A(f + g) = baseChange_A(f) + baseChange_A(g).

Русский

Расширение по основанию сохраняет сумму отображений: baseChange_A(f + g) = baseChange_A(f) + baseChange_A(g).

LaTeX

$$$$\\mathrm{baseChange}_A(f+g)=\\mathrm{baseChange}_A(f)+\\mathrm{baseChange}_A(g).$$$$

Lean4

@[simp]
theorem baseChange_sub : (f - g).baseChange A = f.baseChange A - g.baseChange A :=
  by
  ext
  simp [tmul_sub]

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