Theorems · Definition · field theory

Field.ofMinimalAxioms

(K : Type u) →
  [inst : Add K] →
    [inst_1 : Mul K] →
      [inst_2 : Neg K] →
        [inst_3 : Inv K] →
          [inst_4 : Zero K] →
            [inst_5 : One K] →
              (∀ (a b c : K), a + b + c = a + (b + c)) →
                (∀ (a : K), 0 + a = a) →
                  (∀ (a : K), -a + a = 0) →
                    (∀ (a b c : K), a * b * c = a * (b * c)) →
                      (∀ (a b : K), a * b = b * a) →
                        (∀ (a : K), 1 * a = a) →
                          (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                            0⁻¹ = 0 → (∀ (a b c : K), a * (b + c) = a * b + a * c) → (∃ x y, x ≠ y) → Field K

Define a Field structure on a Type by proving a minimal set of axioms. Note that this uses the default definitions for npow, nsmul, zsmul, div and sub. See note [reducible non-instances].

Defined in

Mathlib.Algebra.Field.MinimalAxioms

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

AddMulNegInvZeroOne