English
If A is a discrete valuation ring and there is a ring equivalence to B, then B is also a discrete valuation ring.
Русский
Если A является дискретным оценочным кольцом и есть кольцо-эквивалентность к B, то и B является DVR.
LaTeX
$$$\mathrm{IsDiscreteValuationRing}(B)$$$
Lean4
theorem isDiscreteValuationRing {A B E : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
[IsDiscreteValuationRing A] [EquivLike E A B] [RingEquivClass E A B] (e : E) : IsDiscreteValuationRing B
where
principal := (isPrincipalIdealRing_iff _).1 <| IsPrincipalIdealRing.of_surjective _ (e : A ≃+* B).surjective
__ : IsLocalRing B := (e : A ≃+* B).isLocalRing
not_a_field' :=
by
obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr <| IsDiscreteValuationRing.not_a_field A)
rw [Submodule.ne_bot_iff]
refine
⟨e a, ⟨?_, by simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero, ha, not_false_eq_true]⟩⟩
rw [IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff e, ← IsLocalRing.mem_maximalIdeal]
exact a.2
