instField — Mathlib

English

The proof of Tilt(K,v,O,hv,p) being a field reduces to showing PreTilt(O,p) has no zero divisors and relating to the field of fractions.

Русский

Доказательство того, что Tilt(K,v,O,hv,p) является полем, сводится к тому, что PreTilt(O,p) не имеет нулевых делителей и соотносится с полем частных.

LaTeX

$$IsDomain(PreTilt(O,p)) and FractionRing.field _$$

Lean4

noncomputable instance [Fact p.Prime] [hvp : Fact (v p ≠ 1)] : Field (Tilt K v O hv p) :=
  haveI := Fact.mk <| mt hv.one_of_isUnit <| (map_natCast (algebraMap O K) p).symm ▸ hvp.1
  haveI := PreTilt.isDomain K v O hv p
  FractionRing.field _

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