smulOneHom_eq_algebraMap — Mathlib

English

The ring hom smulOneHom equals the algebra map: RingHom.smulOneHom = algebraMap R A.

Русский

Кольцо-омон smulOneHom совпадает с алгебраическим отображением: RingHom.smulOneHom = algebraMap R A.

LaTeX

$$$\operatorname{RingHom}.smulOneHom = \operatorname{algebraMap}(R,A)$$$

Lean4

@[simp]
theorem _root_.RingHom.smulOneHom_eq_algebraMap : RingHom.smulOneHom = algebraMap R A :=
  RingHom.ext fun r => (algebraMap_eq_smul_one r).symm

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