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.NatModule (M : Type u) extends Zero M, Add M, HMul Nat M 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
• hMul : Nat → 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.

• zero_hmul (a : M) : 0 * a = 0

  Scalar multiplication by zero is zero.

• one_hmul (a : M) : 1 * a = a

  Scalar multiplication by one is the identity.

• add_hmul (n m : Nat) (a : M) : (n + m) * a = n * a + m * a

  Scalar multiplication is distributive over addition in the natural numbers.

• hmul_zero (n : Nat) : n * 0 = 0

  Scalar multiplication of zero is zero.

• hmul_add (n : Nat) (a b : M) : n * (a + b) = n * a + n * b

  Scalar multiplication is distributive over addition in the module.

class Lean.Grind.IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub 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
• neg : M → M
• sub : M → M → M
• hmulNat : HMul Nat M M

  Scalar multiplication by natural numbers.

• hmulInt : HMul Int M M

  Scalar multiplication by integers.

• 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.

• zero_hmul (a : M) : 0 * a = 0

  Scalar multiplication by zero is zero.

• one_hmul (a : M) : 1 * a = a

  Scalar multiplication by one is the identity.

• add_hmul (n m : Int) (a : M) : (n + m) * a = n * a + m * a

  Scalar multiplication is distributive over addition in the integers.

• hmul_zero (n : Int) : n * 0 = 0

  Scalar multiplication of zero is zero.

• hmul_add (n : Int) (a b : M) : n * (a + b) = n * a + n * b

  Scalar multiplication is distributive over addition in the module.

• 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.

• hmul_nat (n : Nat) (a : M) : ↑n * a = n * a

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

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

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

@[instance 100]

instance Lean.Grind.NatModule.instSMulNat (M : Type u) [NatModule M] : SMul Nat M

Equations

• Lean.Grind.NatModule.instSMulNat M = { smul := fun (a : Nat) (x : M) => a * x }

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.

@[instance 100]

instance Lean.Grind.IntModule.instSMulNat (M : Type u) [IntModule M] : SMul Nat M

Equations

• Lean.Grind.IntModule.instSMulNat M = { smul := fun (a : Nat) (x : M) => a * x }

@[instance 100]

instance Lean.Grind.IntModule.instSMulInt (M : Type u) [IntModule M] : SMul Int M

Equations

• Lean.Grind.IntModule.instSMulInt M = { smul := fun (a : Int) (x : M) => a * x }

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

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

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

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.add_sub_cancel {M : Type u} [IntModule M] {a b : M} : a + b - b = a

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

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)

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

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

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

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

class Lean.Grind.NoNatZeroDivisors (α : Type u) [HMul Nat α α] : 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)] [IntModule α] [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)] [IntModule α] [ToInt.Add α (IntInterval.co lo hi)] [ToInt.Neg α (IntInterval.co lo hi)] : ToInt.Sub α (IntInterval.co lo hi)