lift_mk' — Mathlib

English

Another formulation: if hg 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

/-- Given a commutative ring `A` with field of fractions `K`,
and an injective ring hom `g : A →+* L` where `L` is a field,
field hom induced from `K` to `L` maps `f x / f y` to `g x / g y` for all
`x : A, y ∈ NonZeroDivisors A`. -/
theorem lift_mk' (hg : Injective g) (x) (y : nonZeroDivisors A) : lift hg (mk' K x y) = g x / g y := by
  simp only [mk'_eq_div, map_div₀, lift_algebraMap]

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