coe_subtypeHom' — Mathlib

English

The ring-homomorphism underlying subtypeHom coincides with the subtype's inherent ring hom structure when viewed as a RingHom.

Русский

Тот же базисный кольцевой гомоморфизм, лежащий в основе subtypeHom, совпадает с природной структурой кольцевого гомоморфизма подтипа.

LaTeX

$$$((IsInvariantSubring.subtypeHom M U) : U \\to^* R') = U.subtype$$$

Lean4

@[simp]
theorem coe_subtypeHom' : ((IsInvariantSubring.subtypeHom M U) : U →+* R') = U.subtype :=
  rfl

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