class Lean.Grind.AddRightCancel (M : Type u) [Add M] : Prop

A type where addition is right-cancellative, i.e. a + c = b + c implies a = b.

• add_right_cancel (a b c : M) : a + c = b + c → a = b

  Addition is right-cancellative.

class Lean.Grind.AddCommMonoid (M : Type u) extends Zero M, Add M : Type u

A type with zero and addition, where addition is commutative and associative, and the zero is the right identity for addition.

• zero : M
• add : M → M → M
• add_zero (a : M) : a + 0 = a

  Zero is the right identity for addition.

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

  Addition is commutative.

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

  Addition is associative.

class Lean.Grind.AddCommGroup (M : Type u) extends Lean.Grind.AddCommMonoid M, Neg M, Sub M : Type u

A type with zero, addition, negation, and subtraction, where addition is commutative and associative, and negation is the left inverse of addition.

• zero : M
• add : M → M → M
• add_zero (a : M) : a + 0 = a
• add_comm (a b : M) : a + b = b + a
• add_assoc (a b c : M) : a + b + c = a + (b + c)
• neg : M → M
• sub : M → M → M
• neg_add_cancel (a : M) : -a + a = 0

  Negation is the left inverse of addition.

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

  Subtraction is addition of the negative.

class Lean.Grind.NatModule (M : Type u) extends Lean.Grind.AddCommMonoid M : Type u

A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers, satisfying appropriate compatibilities.

Equivalently, an additive commutative monoid.

Use IntModule if the type has negation.

• zero : M
• add : M → M → M
• add_zero (a : M) : a + 0 = a
• add_comm (a b : M) : a + b = b + a
• add_assoc (a b c : M) : a + b + c = a + (b + c)
• nsmul : SMul Nat M

  Scalar multiplication by natural numbers.

• zero_nsmul (a : M) : 0 • a = 0

  Scalar multiplication by zero is zero.

• add_one_nsmul (n : Nat) (a : M) : (n + 1) • a = n • a + a

  Scalar multiplication by a successor.

class Lean.Grind.IntModule (M : Type u) extends Lean.Grind.AddCommGroup M : Type u

A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers, satisfying appropriate compatibilities.

Equivalently, an additive commutative group.

• zero : M
• add : M → M → M
• add_zero (a : M) : a + 0 = a
• add_comm (a b : M) : a + b = b + a
• add_assoc (a b c : M) : a + b + c = a + (b + c)
• neg : M → M
• sub : M → M → M
• neg_add_cancel (a : M) : -a + a = 0
• sub_eq_add_neg (a b : M) : a - b = a + -b
• nsmul : SMul Nat M

  Scalar multiplication by natural numbers.

• zsmul : SMul Int M

  Scalar multiplication by integers.

• zero_zsmul (a : M) : 0 • a = 0

  Scalar multiplication by zero is zero.

• one_zsmul (a : M) : 1 • a = a

  Scalar multiplication by one is the identity.

• add_zsmul (n m : Int) (a : M) : (n + m) • a = n • a + m • a

  Scalar multiplication is distributive over addition in the integers.

• zsmul_natCast_eq_nsmul (n : Nat) (a : M) : ↑n • a = n • a

  Scalar multiplication by natural numbers is consistent with scalar multiplication by integers.

@[instance 100]

instance Lean.Grind.IntModule.toNatModule {M : Type u} [I : IntModule M] : NatModule M

Equations

• Lean.Grind.IntModule.toNatModule = { toAddCommMonoid := I.toAddCommMonoid, nsmul := Lean.Grind.IntModule.nsmul, zero_nsmul := ⋯, add_one_nsmul := ⋯ }

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Lean.Grind.AddCommGroup.add_sub_cancel {M : Type u} [AddCommGroup M] {a b : M} : a + b - b = a

theorem Lean.Grind.AddCommGroup.sub_add_cancel {M : Type u} [AddCommGroup M] {a b : M} : a - b + b = a

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

theorem Lean.Grind.NatModule.one_nsmul {M : Type u} [NatModule M] (a : M) : 1 • a = a

theorem Lean.Grind.NatModule.add_nsmul {M : Type u} [NatModule M] (n m : Nat) (a : M) : (n + m) • a = n • a + m • a

theorem Lean.Grind.NatModule.nsmul_zero {M : Type u} [NatModule M] (n : Nat) : n • 0 = 0

theorem Lean.Grind.NatModule.nsmul_add {M : Type u} [NatModule M] (n : Nat) (a b : M) : n • (a + b) = n • a + n • b

theorem Lean.Grind.NatModule.mul_nsmul {M : Type u} [NatModule M] (n m : Nat) (a : M) : (n * m) • a = n • m • a

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

theorem Lean.Grind.IntModule.zsmul_zero {M : Type u} [IntModule M] (n : Int) : n • 0 = 0

theorem Lean.Grind.IntModule.zsmul_add {M : Type u} [IntModule M] (n : Int) (a b : M) : n • (a + b) = n • a + n • b

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

theorem Lean.Grind.IntModule.zsmul_sub {M : Type u} [IntModule M] (k : Int) (a b : M) : k • (a - b) = k • a - k • b

theorem Lean.Grind.IntModule.sub_zsmul {M : Type u} [IntModule M] (k₁ k₂ : Int) (a : M) : (k₁ - k₂) • a = k₁ • a - k₂ • a

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

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

We say a module has no natural number zero divisors if k ≠ 0 and k * a = k * b implies a = b (here k is a natural number and a and b are element of the module).

For a module over the integers this is equivalent to k ≠ 0 and k * a = 0 implies a = 0. (See the alternative constructor NoNatZeroDivisors.mk', and the theorem eq_zero_of_mul_eq_zero.)

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

  If k * a ≠ k * b then k ≠ 0 or a ≠ b.

def Lean.Grind.NoNatZeroDivisors.mk' {α : Type u_1} [IntModule α] (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k • a = 0 → a = 0) : NoNatZeroDivisors α

Alternative constructor for NoNatZeroDivisors when we have an IntModule.

Equations

• ⋯ = ⋯

theorem Lean.Grind.NoNatZeroDivisors.eq_zero_of_mul_eq_zero {α : Type u} [NatModule α] [NoNatZeroDivisors α] {k : Nat} {a : α} : k ≠ 0 → k • a = 0 → a = 0

instance Lean.Grind.instNegCoOfZeroOfAdd {α : Type u_1} {lo hi : Int} [ToInt α (IntInterval.co lo hi)] [AddCommGroup α] [ToInt.Zero α (IntInterval.co lo hi)] [ToInt.Add α (IntInterval.co lo hi)] : ToInt.Neg α (IntInterval.co lo hi)

instance Lean.Grind.instSubCoOfAddOfNeg {α : Type u_1} {lo hi : Int} [ToInt α (IntInterval.co lo hi)] [AddCommGroup α] [ToInt.Add α (IntInterval.co lo hi)] [ToInt.Neg α (IntInterval.co lo hi)] : ToInt.Sub α (IntInterval.co lo hi)