English
The algebraic object PreTilt(O, p) is an integral domain under the stated hypotheses (p prime, p not a unit, etc.).
Русский
Алгебраический объект PreTilt(O, p) является целостным доменом при заданных гипотезах (p простое, p не является единицей и т. д.).
LaTeX
$$IsDomain(PreTilt(O,p))$$
Lean4
theorem isDomain : IsDomain (PreTilt O p) :=
by
have hp : Nat.Prime p := Fact.out
haveI : Nontrivial (PreTilt O p) := ⟨(CharP.nontrivial_of_char_ne_one hp.ne_one).1⟩
haveI : NoZeroDivisors (PreTilt O p) :=
⟨fun hfg => by
simp_rw [← map_eq_zero hv] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
exact mul_ne_zero hfg.1 hfg.2⟩
exact NoZeroDivisors.to_isDomain _
