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.CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat α : Type u

• add : α → α → α
• mul : α → α → α
• neg : α → α
• sub : α → α → α
• hPow : α → Nat → α
• ofNat (n : Nat) : OfNat α n
• natCast : NatCast α
• intCast : IntCast α
• 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
• neg_add_cancel (a : α) : -a + a = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• mul_comm (a b : α) : a * b = b * a
• mul_one (a : α) : a * 1 = a
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• zero_mul (a : α) : 0 * a = 0
• sub_eq_add_neg (a b : α) : a - b = a + -b
• 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
• intCast_ofNat (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n
• intCast_neg (i : Int) : ↑(-i) = -↑i

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

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

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

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

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

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

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

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

theorem Lean.Grind.CommRing.one_mul {α : Type u} [CommRing α] (a : α) : 1 * a = a

theorem Lean.Grind.CommRing.right_distrib {α : Type u} [CommRing α] (a b c : α) : (a + b) * c = a * c + b * c

theorem Lean.Grind.CommRing.mul_zero {α : Type u} [CommRing α] (a : α) : a * 0 = 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• ofNat_eq_zero_iff (x : Nat) : OfNat.ofNat x = 0 ↔ x % p = 0

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

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

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

theorem Lean.Grind.IsCharP.ofNat_ext_iff (p : Nat) {α : Type u} [CommRing α] [IsCharP α p] {x y : Nat} : OfNat.ofNat x = OfNat.ofNat y ↔ x % p = y % p

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

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

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

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

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

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

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

theorem Lean.Grind.IsCharP.ofNat_eq_iff_of_lt (p : Nat) {α : Type u} [CommRing α] [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_of_lt (p : Nat) {α : Type u} [CommRing α] [IsCharP α p] {x : Nat} (h : x < p) : ↑x = 0 ↔ x = 0

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

class Lean.Grind.NoNatZeroDivisors (α : Type u) [CommRing α] : Prop

Special case of Mathlib's NoZeroSMulDivisors Nat α.

• no_nat_zero_divisors (k : Nat) (a : α) : k ≠ 0 → OfNat.ofNat k * a = 0 → a = 0

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