English
If R is a commutative ring and hR is a HenselianLocalRing on R, then the ring (R, maximalIdeal R) carries a HenselianRing structure.
Русский
Пусть R — коммутативное кольцо и hR — гензелевское локальное кольцо на R, тогда пара (R, maximalIdeal R) образует гензелеву структуру кольца.
LaTeX
$$$\forall R [CommRing R] [hR : HenselianLocalRing R], \; HenselianRing(R, \operatorname{maximalIdeal} R).$$$
Lean4
instance (R : Type*) [CommRing R] [hR : HenselianLocalRing R] : HenselianRing R (maximalIdeal R)
where
jac := by
rw [Ideal.jacobson, le_sInf_iff]
rintro I ⟨-, hI⟩
exact (eq_maximalIdeal hI).ge
is_henselian := by
intro f hf a₀ h₁ h₂
refine HenselianLocalRing.is_henselian f hf a₀ h₁ ?_
contrapose! h₂
rw [← mem_nonunits_iff, ← IsLocalRing.mem_maximalIdeal, ← Ideal.Quotient.eq_zero_iff_mem] at h₂
rw [h₂]
exact not_isUnit_zero
