Documentation

Init.Grind.CommRing.Basic

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 α :
  • 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
Instances
    class Lean.Grind.Ring (α : Type u) extends Lean.Grind.Semiring α, Neg α, Sub α :
    Instances
      Instances
        Instances
          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.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.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
          Equations
            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) :
            Instances
              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} :
              theorem Lean.Grind.IsCharP.ofNat_ext (p : Nat) {α : Type u} [Ring α] [IsCharP α p] {x y : Nat} (h : x % p = y % p) :
              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) :
              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) :
              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 0k * a = 0a = 0