lift_fieldRange — Mathlib

English

If hg is injective and g.range = Subring.closure s, then (lift hg).fieldRange = Subfield.closure s.

Русский

Пусть hg инъективно, и g.range = Subring.closure s. Тогда (lift hg).fieldRange = Subfield.closure s.

LaTeX

$$$ (\mathrm{lift} \; hg).fieldRange = \operatorname{Subfield.closure} s $$$

Lean4

/-- The image of `IsFractionRing.lift` is the subfield generated by the image
of the ring hom. -/
theorem lift_fieldRange (hg : Injective g) : (lift hg : K →+* L).fieldRange = Subfield.closure g.range :=
  ringHom_fieldRange_eq_of_comp_eq (by ext; simp)

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