English
There is a Field structure on a type K provided with a minimal set of axioms; equivalently, Field K can be generated from a small list of axioms.
Русский
На типе K имеется структура поля, задаваемая минимальным набором аксиом; полное поле определяется малыми аксиомами.
LaTeX
$$$\exists Field\,K$ с минимальными аксиомами \,(add, mul, neg, inv, zero, one, and the listed axioms)$$$
Lean4
/-- Define a `Field` structure on a Type by proving a minimized set of axioms.
Note that this uses the default definitions for `npow`, `nsmul`, `zsmul`, `div` and `sub`.
See note [reducible non-instances]. -/
abbrev ofMinimalAxioms (K : Type u) [Add K] [Mul K] [Neg K] [Inv K] [Zero K] [One K]
(add_assoc : ∀ a b c : K, a + b + c = a + (b + c)) (zero_add : ∀ a : K, 0 + a = a)
(neg_add_cancel : ∀ a : K, -a + a = 0) (mul_assoc : ∀ a b c : K, a * b * c = a * (b * c))
(mul_comm : ∀ a b : K, a * b = b * a) (one_mul : ∀ a : K, 1 * a = a) (mul_inv_cancel : ∀ a : K, a ≠ 0 → a * a⁻¹ = 1)
(inv_zero : (0 : K)⁻¹ = 0) (left_distrib : ∀ a b c : K, a * (b + c) = a * b + a * c)
(exists_pair_ne : ∃ x y : K, x ≠ y) : Field K :=
letI := CommRing.ofMinimalAxioms add_assoc zero_add neg_add_cancel mul_assoc mul_comm one_mul left_distrib
{ exists_pair_ne := exists_pair_ne
mul_inv_cancel := mul_inv_cancel
inv_zero := inv_zero
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl }
