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

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• ofNat (n : Nat) : OfNat α n
• natCast : NatCast α
• 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

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

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• ofNat (n : Nat) : OfNat α n
• natCast : NatCast α
• 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

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

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• ofNat (n : Nat) : OfNat α n
• natCast : NatCast α
• 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

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

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• ofNat (n : Nat) : OfNat α n
• natCast : NatCast α
• 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₂

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_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.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) [Ring α] (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} [Ring α] [IsCharP α p] (x : Nat) : ↑x = 0 ↔ x % p = 0

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.ofNat_ext_iff (p : Nat) {α : Type u} [Ring α] [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} [Ring α] [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} [Ring α] [IsCharP α p] {x y : Nat} (h : x % p = y % p) : ↑x = ↑y

theorem Lean.Grind.IsCharP.natCast_ext_iff (p : Nat) {α : Type u} [Ring α] [IsCharP α p] {x y : Nat} : ↑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.IsCharP.natCast_emod (p : Nat) {α : Type u} [Ring α] [IsCharP α p] (x : Nat) : ↑(x % p) = ↑x

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

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

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