English
If R is a Domain and Artinian, then R is a Field.
Русский
Если R — домен и артиново кольцо, то R является полем.
LaTeX
$$$[IsDomain R] \Rightarrow [IsArtinianRing R] \Rightarrow IsField R$$$
Lean4
theorem isField_of_isDomain [IsDomain R] : IsField R :=
by
refine ⟨Nontrivial.exists_pair_ne, mul_comm, fun {x} hx ↦ ?_⟩
obtain ⟨n, y, hy⟩ := IsArtinian.exists_pow_succ_smul_dvd x (1 : R)
replace hy : x ^ n * (x * y - 1) = 0 := by
rw [mul_sub, sub_eq_zero]
convert hy using 1
simp [Nat.succ_eq_add_one, pow_add, mul_assoc]
rw [mul_eq_zero, sub_eq_zero] at hy
exact
⟨_, hy.resolve_left <| pow_ne_zero _ hx⟩
/- Does not hold in a commutative semiring:
consider {0, 0.5, 1} with ⊔ as + and ⊓ as *, then both {0} and {0, 0.5} are prime ideals. -/
-- Note: type class synthesis should try to synthesize `p.IsPrime` before `IsArtinianRing R`,
-- hence the argument order.
