algebraMap_eq — Mathlib

English

The algebra maps form a coherent tower: algebraMap R A = (algebraMap S A) ∘ (algebraMap R S).

Русский

Согласованная башня алгебраических отображений: algebraMap R A = (algebraMap S A) ∘ (algebraMap R S).

LaTeX

$$$\mathrm{algebraMap}\;R\;A = (\mathrm{algebraMap}\;S\;A) \circ (\mathrm{algebraMap}\;R\;S)$$$

Lean4

theorem algebraMap_eq : algebraMap R A = (algebraMap S A).comp (algebraMap R S) :=
  RingHom.ext fun x => by simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

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