class Lean.Grind.NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M : Type u

• zero : M
• add : M → M → M
• hMul : Nat → M → M
• add_zero (a : M) : a + 0 = a
• zero_add (a : M) : 0 + a = a
• add_comm (a b : M) : a + b = b + a
• add_assoc (a b c : M) : a + b + c = a + (b + c)
• zero_hmul (a : M) : 0 * a = 0
• one_hmul (a : M) : 1 * a = a
• add_hmul (n m : Nat) (a : M) : (n + m) * a = n * a + m * a
• hmul_zero (n : Nat) : n * 0 = 0
• hmul_add (n : Nat) (a b : M) : n * (a + b) = n * a + n * b
• mul_hmul (n m : Nat) (a : M) : n * m * a = n * (m * a)

Instances

• Lean.Grind.IntModule.toNatModule
• Lean.Grind.Semiring.instNatModule

class Lean.Grind.IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M : Type u

• zero : M
• add : M → M → M
• neg : M → M
• sub : M → M → M
• hMul : Int → M → M
• add_zero (a : M) : a + 0 = a
• zero_add (a : M) : 0 + a = a
• add_comm (a b : M) : a + b = b + a
• add_assoc (a b c : M) : a + b + c = a + (b + c)
• zero_hmul (a : M) : 0 * a = 0
• one_hmul (a : M) : 1 * a = a
• add_hmul (n m : Int) (a : M) : (n + m) * a = n * a + m * a
• hmul_zero (n : Int) : n * 0 = 0
• hmul_add (n : Int) (a b : M) : n * (a + b) = n * a + n * b
• mul_hmul (n m : Int) (a : M) : n * m * a = n * (m * a)
• neg_add_cancel (a : M) : -a + a = 0
• sub_eq_add_neg (a b : M) : a - b = a + -b

Instances

• Lean.Grind.Ring.instIntModule

instance Lean.Grind.IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M

Equations

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

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

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

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

theorem Lean.Grind.IntModule.neg_zero {M : Type u} [IntModule M] : -0 = 0

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

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

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

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

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

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

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

theorem Lean.Grind.IntModule.neg_hmul {M : Type u} [IntModule M] (n : Int) (a : M) : -n * a = -(n * a)

theorem Lean.Grind.IntModule.hmul_neg {M : Type u} [IntModule M] (n : Int) (a : M) : n * -a = -(n * a)

class Lean.Grind.NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] : Prop

Special case of Mathlib's NoZeroSMulDivisors Nat α.

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

Instances

• Lean.Grind.Field.instNoNatZeroDivisorsOfIsCharPOfNatNat
• Lean.Grind.instNoNatZeroDivisorsInt