English
The generic instance declaring that the theory of fields models on K when K is a field with compatible ring structure.
Русский
Общий экземпляр указывает, что теория полей моделируется на K, когда K — поле с совместимой кольцевой структурой.
LaTeX
$$$[Field K] \Rightarrow \text{Theory.field.Model } K$$$
Lean4
instance [Field K] [CompatibleRing K] : Theory.field.Model K :=
{
realize_of_mem := by
simp only [Theory.field, Set.mem_range, exists_imp]
rintro φ a rfl
rw [a.realize_toSentence_iff_toProp (K := K)]
cases a with
| existsPairNE => exact exists_pair_ne K
| existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩
| addAssoc => exact add_assoc
| zeroAdd => exact zero_add
| negAddCancel => exact neg_add_cancel
| mulAssoc => exact mul_assoc
| mulComm => exact mul_comm
| oneMul => exact one_mul
| leftDistrib => exact mul_add }
