English
The instances given by fieldOfModelField are compatible with the ring structure on the type K, ensuring a coherent field structure on models.
Русский
Инстанции, задаваемые fieldOfModelField, совместимы с кольцевой структурой на K, образуя согласованную структуру поля на моделях.
LaTeX
$$$\text{CompatibleRing}(K)$$$
Lean4
/-- A model for the theory of fields is a field. To introduced locally on Types that don't
already have instances for ring operations.
When this is used, it is almost always useful to also add locally the instance
`compatibleFieldOfModelField` afterwards. -/
noncomputable abbrev fieldOfModelField (K : Type*) [Language.ring.Structure K] [Theory.field.Model K] : Field K :=
letI : DecidableEq K := Classical.decEq K
letI := addOfRingStructure K
letI := mulOfRingStructure K
letI := negOfRingStructure K
letI := zeroOfRingStructure K
letI := oneOfRingStructure K
letI := compatibleRingOfRingStructure K
have exists_inv : ∀ x : K, x ≠ 0 → ∃ y : K, x * y = 1 := existsInv.toProp_of_model
letI : Inv K := ⟨fun x => if hx0 : x = 0 then 0 else Classical.choose (exists_inv x hx0)⟩
Field.ofMinimalAxioms K addAssoc.toProp_of_model zeroAdd.toProp_of_model negAddCancel.toProp_of_model
mulAssoc.toProp_of_model mulComm.toProp_of_model oneMul.toProp_of_model
(fun x hx0 =>
show x * (dite _ _ _) = _ from (dif_neg hx0).symm ▸ Classical.choose_spec (existsInv.toProp_of_model x hx0))
(dif_pos rfl) leftDistrib.toProp_of_model existsPairNE.toProp_of_model
