A monolithic commutative ring typeclass for internal use in grind.

The Lean.Grind.CommRing class will be used to convert expressions into the internal representation via polynomials, with coefficients expressed via OfNat and Neg.

The IsCharP α p typeclass expresses that the ring has characteristic p, i.e. that a coefficient OfNat.ofNat x : α is zero if and only if x % p = 0 (in Nat). See

theorem ofNat_ext_iff {x y : Nat} : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p
theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x
theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
    OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x = y

class Lean.Grind.Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α : Type u

A semiring, i.e. a type equipped with addition, multiplication, and a map from the natural numbers, satisfying appropriate compatibilities.

Use Ring instead if the type also has negation, CommSemiring if the multiplication is commutative, or CommRing if the type has negation and multiplication is commutative.

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• natCast : NatCast α

  In every semiring there is a canonical map from the natural numbers to the semiring, providing the values of 0 and 1. Note that this function need not be injective.

• ofNat (n : Nat) : OfNat α n

  Natural number numerals in the semiring. The field ofNat_eq_natCast ensures that these are (propositionally) equal to the values of natCast.

• add_assoc (a b c : α) : a + b + c = a + (b + c)

  Addition is associative.

• add_comm (a b : α) : a + b = b + a

  Addition is commutative.

• add_zero (a : α) : a + 0 = a

  Zero is the right identity for addition.

• mul_assoc (a b c : α) : a * b * c = a * (b * c)

  Multiplication is associative.

• mul_one (a : α) : a * 1 = a

  One is the right identity for multiplication.

• one_mul (a : α) : 1 * a = a

  One is the left identity for multiplication.

• left_distrib (a b c : α) : a * (b + c) = a * b + a * c

  Left distributivity of multiplication over addition.

• right_distrib (a b c : α) : (a + b) * c = a * c + b * c

  Right distributivity of multiplication over addition.

• zero_mul (a : α) : 0 * a = 0

  Zero is right absorbing for multiplication.

• mul_zero (a : α) : a * 0 = 0

  Zero is left absorbing for multiplication.

• pow_zero (a : α) : a ^ 0 = 1

  The zeroth power of any element is one.

• pow_succ (a : α) (n : Nat) : a ^ (n + 1) = a ^ n * a

  The successor power law for exponentiation.

• ofNat_succ (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1

  Numerals are consistently defined with respect to addition.

• ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = ↑n

  Numerals are consistently defined with respect to the canonical map from natural numbers.

class Lean.Grind.Ring (α : Type u) extends Lean.Grind.Semiring α, Neg α, Sub α : Type u

A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers, satisfying appropriate compatibilities.

Use CommRing if the multiplication is commutative.

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• natCast : NatCast α
• ofNat (n : Nat) : OfNat α n
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• add_comm (a b : α) : a + b = b + a
• add_zero (a : α) : a + 0 = a
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• mul_one (a : α) : a * 1 = a
• one_mul (a : α) : 1 * a = a
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• pow_zero (a : α) : a ^ 0 = 1
• pow_succ (a : α) (n : Nat) : a ^ (n + 1) = a ^ n * a
• ofNat_succ (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
• ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = ↑n
• neg : α → α
• sub : α → α → α
• intCast : IntCast α

  In every ring there is a canonical map from the integers to the ring.

• neg_add_cancel (a : α) : -a + a = 0

  Negation is the left inverse of addition.

• sub_eq_add_neg (a b : α) : a - b = a + -b

  Subtraction is addition of the negative.

• intCast_ofNat (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n

  The canonical map from the integers is consistent with the canonical map from the natural numbers.

• intCast_neg (i : Int) : ↑(-i) = -↑i

  The canonical map from the integers is consistent with negation.

class Lean.Grind.CommSemiring (α : Type u) extends Lean.Grind.Semiring α : Type u

A commutative semiring, i.e. a semiring with commutative multiplication.

Use CommRing if the type has negation.

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• natCast : NatCast α
• ofNat (n : Nat) : OfNat α n
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• add_comm (a b : α) : a + b = b + a
• add_zero (a : α) : a + 0 = a
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• mul_one (a : α) : a * 1 = a
• one_mul (a : α) : 1 * a = a
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• pow_zero (a : α) : a ^ 0 = 1
• pow_succ (a : α) (n : Nat) : a ^ (n + 1) = a ^ n * a
• ofNat_succ (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
• ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = ↑n
• mul_comm (a b : α) : a * b = b * a

  Multiplication is commutative.

class Lean.Grind.CommRing (α : Type u) extends Lean.Grind.Ring α, Lean.Grind.CommSemiring α : Type u

A commutative ring, i.e. a ring with commutative multiplication.

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• natCast : NatCast α
• ofNat (n : Nat) : OfNat α n
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• add_comm (a b : α) : a + b = b + a
• add_zero (a : α) : a + 0 = a
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• mul_one (a : α) : a * 1 = a
• one_mul (a : α) : 1 * a = a
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• pow_zero (a : α) : a ^ 0 = 1
• pow_succ (a : α) (n : Nat) : a ^ (n + 1) = a ^ n * a
• ofNat_succ (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
• ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = ↑n
• neg : α → α
• sub : α → α → α
• intCast : IntCast α
• neg_add_cancel (a : α) : -a + a = 0
• sub_eq_add_neg (a b : α) : a - b = a + -b
• intCast_ofNat (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n
• intCast_neg (i : Int) : ↑(-i) = -↑i
• mul_comm (a b : α) : a * b = b * a

theorem Lean.Grind.Semiring.natCast_zero {α : Type u} [Semiring α] : ↑0 = 0

theorem Lean.Grind.Semiring.natCast_one {α : Type u} [Semiring α] : ↑1 = 1

theorem Lean.Grind.Semiring.ofNat_add {α : Type u} [Semiring α] (a b : Nat) : OfNat.ofNat (a + b) = OfNat.ofNat a + OfNat.ofNat b

theorem Lean.Grind.Semiring.natCast_add {α : Type u} [Semiring α] (a b : Nat) : ↑(a + b) = ↑a + ↑b

theorem Lean.Grind.Semiring.natCast_succ {α : Type u} [Semiring α] (n : Nat) : ↑(n + 1) = ↑n + 1

theorem Lean.Grind.Semiring.zero_add {α : Type u} [Semiring α] (a : α) : 0 + a = a

theorem Lean.Grind.Semiring.add_left_comm {α : Type u} [Semiring α] (a b c : α) : a + (b + c) = b + (a + c)

theorem Lean.Grind.Semiring.ofNat_mul {α : Type u} [Semiring α] (a b : Nat) : OfNat.ofNat (a * b) = OfNat.ofNat a * OfNat.ofNat b

theorem Lean.Grind.Semiring.natCast_mul {α : Type u} [Semiring α] (a b : Nat) : ↑(a * b) = ↑a * ↑b

theorem Lean.Grind.Semiring.pow_one {α : Type u} [Semiring α] (a : α) : a ^ 1 = a

theorem Lean.Grind.Semiring.pow_two {α : Type u} [Semiring α] (a : α) : a ^ 2 = a * a

theorem Lean.Grind.Semiring.pow_add {α : Type u} [Semiring α] (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a ^ k₁ * a ^ k₂

theorem Lean.Grind.Semiring.natCast_pow {α : Type u} [Semiring α] (x k : Nat) : ↑(x ^ k) = ↑x ^ k

instance Lean.Grind.Semiring.instNatModule {α : Type u} [Semiring α] : NatModule α

Equations

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

theorem Lean.Grind.Semiring.hmul_eq_natCast_mul {α : Type u_1} [Semiring α] {k : Nat} {a : α} : k * a = ↑k * a

theorem Lean.Grind.Semiring.hmul_eq_ofNat_mul {α : Type u_1} [Semiring α] {k : Nat} {a : α} : k * a = OfNat.ofNat k * a

theorem Lean.Grind.Ring.add_neg_cancel {α : Type u} [Ring α] (a : α) : a + -a = 0

theorem Lean.Grind.Ring.add_left_inj {α : Type u} [Ring α] {a b : α} (c : α) : a + c = b + c ↔ a = b

theorem Lean.Grind.Ring.add_right_inj {α : Type u} [Ring α] (a b c : α) : a + b = a + c ↔ b = c

theorem Lean.Grind.Ring.neg_zero {α : Type u} [Ring α] : -0 = 0

theorem Lean.Grind.Ring.neg_neg {α : Type u} [Ring α] (a : α) : - -a = a

theorem Lean.Grind.Ring.neg_eq_zero {α : Type u} [Ring α] (a : α) : -a = 0 ↔ a = 0

theorem Lean.Grind.Ring.neg_eq_iff {α : Type u} [Ring α] (a b : α) : -a = b ↔ a = -b

theorem Lean.Grind.Ring.neg_add {α : Type u} [Ring α] (a b : α) : -(a + b) = -a + -b

theorem Lean.Grind.Ring.neg_sub {α : Type u} [Ring α] (a b : α) : -(a - b) = b - a

theorem Lean.Grind.Ring.sub_self {α : Type u} [Ring α] (a : α) : a - a = 0

theorem Lean.Grind.Ring.sub_eq_iff {α : Type u} [Ring α] {a b c : α} : a - b = c ↔ a = c + b

theorem Lean.Grind.Ring.sub_eq_zero_iff {α : Type u} [Ring α] {a b : α} : a - b = 0 ↔ a = b

theorem Lean.Grind.Ring.intCast_zero {α : Type u} [Ring α] : ↑0 = 0

theorem Lean.Grind.Ring.intCast_one {α : Type u} [Ring α] : ↑1 = 1

theorem Lean.Grind.Ring.intCast_neg_one {α : Type u} [Ring α] : ↑(-1) = -1

theorem Lean.Grind.Ring.intCast_natCast {α : Type u} [Ring α] (n : Nat) : ↑↑n = ↑n

theorem Lean.Grind.Ring.intCast_natCast_add_one {α : Type u} [Ring α] (n : Nat) : ↑(↑n + 1) = ↑n + 1

theorem Lean.Grind.Ring.intCast_negSucc {α : Type u} [Ring α] (n : Nat) : ↑(-(↑n + 1)) = -(↑n + 1)

theorem Lean.Grind.Ring.intCast_nat_add {α : Type u} [Ring α] {x y : Nat} : ↑(↑x + ↑y) = ↑x + ↑y

theorem Lean.Grind.Ring.intCast_nat_sub {α : Type u} [Ring α] {x y : Nat} (h : x ≥ y) : ↑↑(x - y) = ↑x - ↑y

theorem Lean.Grind.Ring.intCast_add {α : Type u} [Ring α] (x y : Int) : ↑(x + y) = ↑x + ↑y

theorem Lean.Grind.Ring.intCast_sub {α : Type u} [Ring α] (x y : Int) : ↑(x - y) = ↑x - ↑y

theorem Lean.Grind.Ring.ofNat_sub {α : Type u} [Ring α] {x y : Nat} (h : y ≤ x) : OfNat.ofNat (x - y) = OfNat.ofNat x - OfNat.ofNat y

theorem Lean.Grind.Ring.neg_ofNat_sub {α : Type u} [Ring α] {x y : Nat} (h : y ≤ x) : -OfNat.ofNat (x - y) = OfNat.ofNat y - OfNat.ofNat x

theorem Lean.Grind.Ring.neg_eq_neg_one_mul {α : Type u} [Ring α] (a : α) : -a = -1 * a

theorem Lean.Grind.Ring.neg_eq_mul_neg_one {α : Type u} [Ring α] (a : α) : -a = a * -1

theorem Lean.Grind.Ring.neg_mul {α : Type u} [Ring α] (a b : α) : -a * b = -(a * b)

theorem Lean.Grind.Ring.mul_neg {α : Type u} [Ring α] (a b : α) : a * -b = -(a * b)

theorem Lean.Grind.Ring.intCast_nat_mul {α : Type u} [Ring α] (x y : Nat) : ↑(↑x * ↑y) = ↑x * ↑y

theorem Lean.Grind.Ring.intCast_mul {α : Type u} [Ring α] (x y : Int) : ↑(x * y) = ↑x * ↑y

theorem Lean.Grind.Ring.intCast_pow {α : Type u} [Ring α] (x : Int) (k : Nat) : ↑(x ^ k) = ↑x ^ k

instance Lean.Grind.Ring.instIntModule {α : Type u} [Ring α] : IntModule α

Equations

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

theorem Lean.Grind.Ring.hmul_eq_intCast_mul {α : Type u_1} [Ring α] {k : Int} {a : α} : k * a = ↑k * a

theorem Lean.Grind.CommSemiring.mul_left_comm {α : Type u} [CommSemiring α] (a b c : α) : a * (b * c) = b * (a * c)

class Lean.Grind.IsCharP (α : Type u) [Semiring α] (p : outParam Nat) : Prop

A ring α has characteristic p if OfNat.ofNat x = 0 iff x % p = 0.

Note that for p = 0, we have x % p = x, so this says that OfNat.ofNat is injective from Nat to α.

In the case of a semiring, we take the stronger condition that OfNat.ofNat x = OfNat.ofNat y iff x % p = y % p.

• ofNat_ext_iff {x y : Nat} : OfNat.ofNat x = OfNat.ofNat y ↔ x % p = y % p

  Two numerals in a semiring are equal iff they are congruent module p in the natural numbers.

theorem Lean.Grind.IsCharP.ofNat_eq_zero_iff {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] (x : Nat) : OfNat.ofNat x = 0 ↔ x % p = 0

theorem Lean.Grind.IsCharP.ofNat_ext {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x y : Nat} (h : x % p = y % p) : OfNat.ofNat x = OfNat.ofNat y

theorem Lean.Grind.IsCharP.ofNat_eq_zero_iff_of_lt {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x : Nat} (h : x < p) : OfNat.ofNat x = 0 ↔ x = 0

theorem Lean.Grind.IsCharP.ofNat_eq_iff_of_lt {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x y : Nat} (h₁ : x < p) (h₂ : y < p) : OfNat.ofNat x = OfNat.ofNat y ↔ x = y

theorem Lean.Grind.IsCharP.natCast_eq_zero_iff {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] (x : Nat) : ↑x = 0 ↔ x % p = 0

theorem Lean.Grind.IsCharP.natCast_ext {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x y : Nat} (h : x % p = y % p) : ↑x = ↑y

theorem Lean.Grind.IsCharP.natCast_ext_iff {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x y : Nat} : ↑x = ↑y ↔ x % p = y % p

theorem Lean.Grind.IsCharP.natCast_emod {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] (x : Nat) : ↑(x % p) = ↑x

theorem Lean.Grind.IsCharP.ofNat_emod {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] (x : Nat) : OfNat.ofNat (x % p) = OfNat.ofNat x

theorem Lean.Grind.IsCharP.natCast_eq_zero_iff_of_lt {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x : Nat} (h : x < p) : ↑x = 0 ↔ x = 0

theorem Lean.Grind.IsCharP.natCast_eq_iff_of_lt {α : Type u_1} (p : Nat) [Semiring α] [IsCharP α p] {x y : Nat} (h₁ : x < p) (h₂ : y < p) : ↑x = ↑y ↔ x = y

def Lean.Grind.IsCharP.mk' (p : Nat) (α : Type u) [Ring α] (ofNat_eq_zero_iff : ∀ (x : Nat), OfNat.ofNat x = 0 ↔ x % p = 0) : IsCharP α p

Alternative constructor when α is a Ring.

Equations

• ⋯ = ⋯

theorem Lean.Grind.IsCharP.intCast_eq_zero_iff (p : Nat) {α : Type u} [Ring α] [IsCharP α p] (x : Int) : ↑x = 0 ↔ x % ↑p = 0

theorem Lean.Grind.IsCharP.intCast_ext_iff (p : Nat) {α : Type u} [Ring α] [IsCharP α p] {x y : Int} : ↑x = ↑y ↔ x % ↑p = y % ↑p

theorem Lean.Grind.IsCharP.intCast_emod (p : Nat) {α : Type u} [Ring α] [IsCharP α p] (x : Int) : ↑(x % ↑p) = ↑x

theorem Lean.Grind.no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α} : k ≠ 0 → k * a = 0 → a = 0