coe_subtypeHom — Mathlib

English

The underlying function of subtypeHom is just the inclusion map, i.e., the coercion from the invariant subring to R'.

Русский

Основная функция subtypeHom совпадает с включением, то есть замену подструктуры на R'.

LaTeX

$$$\\text{coe_subtypeHom} : (IsInvariantSubring.subtypeHom M U) = \\mathrm{Subtype}.val$$$

Lean4

@[simp]
theorem coe_subtypeHom : (IsInvariantSubring.subtypeHom M U : U → R') = Subtype.val :=
  rfl

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