baseChange_mul — Mathlib

English

Base-change preserves multiplication of endomorphisms: baseChange_A(fg) = baseChange_A(f) baseChange_A(g).

Русский

Расширение сохраняет умножение концевых отображений: baseChange_A(fg) = baseChange_A(f) baseChange_A(g).

LaTeX

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

Lean4

theorem baseChange_mul (f g : Module.End R M) : (f * g).baseChange A = f.baseChange A * g.baseChange A := by ext; simp

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