Minimal Axioms for a Ring

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

Main Definitions

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

@[reducible]

def Ring.ofMinimalAxioms {R : Type u} [Add R] [Mul R] [Neg R] [Zero R] [One R] (add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)) (zero_add : ∀ (a : R), 0 + a = a) (add_left_neg : ∀ (a : R), -a + a = 0) (mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)) (one_mul : ∀ (a : R), 1 * a = a) (mul_one : ∀ (a : R), a * 1 = a) (left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c) (right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c) : Ring R

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

Equations

• Ring.ofMinimalAxioms add_assoc zero_add add_left_neg mul_assoc one_mul mul_one left_distrib right_distrib = Ring.mk zsmulRec add_left_neg

@[reducible]

def CommRing.ofMinimalAxioms {R : Type u} [Add R] [Mul R] [Neg R] [Zero R] [One R] (add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)) (zero_add : ∀ (a : R), 0 + a = a) (add_left_neg : ∀ (a : R), -a + a = 0) (mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)) (mul_comm : ∀ (a b : R), a * b = b * a) (one_mul : ∀ (a : R), 1 * a = a) (left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c) : CommRing R

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

Equations

• CommRing.ofMinimalAxioms add_assoc zero_add add_left_neg mul_assoc mul_comm one_mul left_distrib = CommRing.mk mul_comm