baseChange_add — Mathlib

English

Base-change is additive in f: 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_add : (f + g).baseChange A = f.baseChange A + g.baseChange A :=
  by
  ext
  simp [baseChange_eq_ltensor, -baseChange_tmul]

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