Minimal Axioms for a Field

This file defines constructors to define a Field structure on a Type, while proving a minimum number of equalities.

Main Definitions

• Field.ofMinimalAxioms: Define a Field structure on a Type by proving a minimized set of axioms

@[reducible]

def Field.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) (add_left_neg : ∀ (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⁻¹ = 0) (left_distrib : ∀ (a b c : K), a * (b + c) = a * b + a * c) (exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y) : Field K

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].

Equations

• One or more equations did not get rendered due to their size.