toRingHom_mapRangeAlgHom — Mathlib

English

The underlying ring hom of mapRangeAlgHom coincides with mapRangeRingHom on the level of the base ring: RingHom equivalence aligns with its ring-hom counterpart.

Русский

Прямой переход от mapRangeAlgHom к mapRangeRingHom согласуется на уровне колец: соответствие кольцевых гомоморфизмов совпадает.

LaTeX

$$$\\mathrm{toRingHom} (\\mathrm{MonoidAlgebra.mapRangeAlgHom\\ M f}) = \\mathrm{MonoidAlgebra.mapRangeRingHom\\ M f.toRingHom}$$$

Lean4

@[to_additive (attr := simp)]
theorem toRingHom_mapRangeAlgHom (f : A →ₐ[R] B) : mapRangeAlgHom M f = mapRangeRingHom M f.toRingHom :=
  rfl

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