Documentation

Init.Grind.Module.Envelope

theorem Lean.Grind.IntModule.OfNatModule.instAssociativeHAdd (α : Type u) [NatModule α] :

Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.IntModule.OfNatModule.instCommutativeHAdd (α : Type u) [NatModule α] :

Std.Commutative fun (x1 x2 : α) => x1 + x2

def Lean.Grind.IntModule.OfNatModule.r (α : Type u) [NatModule α] :

α × α → α × α → Prop

Equations

Lean.Grind.IntModule.OfNatModule.r α (a, b) (c, d) = ∃ (k : α), a + d + k = b + c + k

Instances For

def Lean.Grind.IntModule.OfNatModule.Q (α : Type u) [NatModule α] :

Equations

Lean.Grind.IntModule.OfNatModule.Q α = Quot (Lean.Grind.IntModule.OfNatModule.r α)

Instances For

theorem Lean.Grind.IntModule.OfNatModule.r_rfl {α : Type u} [NatModule α] (a : α × α) :

r α a a

theorem Lean.Grind.IntModule.OfNatModule.r_sym {α : Type u} [NatModule α] {a b : α × α} :

r α a b → r α b a

theorem Lean.Grind.IntModule.OfNatModule.r_trans {α : Type u} [NatModule α] {a b c : α × α} :

r α a b → r α b c → r α a c

def Lean.Grind.IntModule.OfNatModule.Q.mk {α : Type u} [NatModule α] (p : α × α) :

Q α

Equations

Lean.Grind.IntModule.OfNatModule.Q.mk p = Quot.mk (Lean.Grind.IntModule.OfNatModule.r α) p

Instances For

def Lean.Grind.IntModule.OfNatModule.Q.liftOn₂ {α : Type u} [NatModule α] {β : Sort u_1} (q₁ q₂ : Q α) (f : α × α → α × α → β) (h : ∀ {a₁ b₁ a₂ b₂ : α × α}, r α a₁ a₂ → r α b₁ b₂ → f a₁ b₁ = f a₂ b₂) :

β

Equations

q₁.liftOn₂ q₂ f h = Quot.lift (fun (a₁ : α × α) => Quot.lift (f a₁) ⋯ q₂) ⋯ q₁

Instances For

def Lean.Grind.IntModule.OfNatModule.Q.ind {α : Type u} [NatModule α] {β : Q α → Prop} (mk : ∀ (a : α × α), β (mk a)) (q : Q α) :

β q

Equations

⋯ = ⋯

Instances For

def Lean.Grind.IntModule.OfNatModule.nsmul {α : Type u} [NatModule α] (n : Nat) (q : Q α) :

Q α

Equations

Lean.Grind.IntModule.OfNatModule.nsmul n q = Quot.liftOn q (fun (x : α × α) => match x with | (a, b) => Lean.Grind.IntModule.OfNatModule.Q.mk (n • a, n • b)) ⋯

Instances For

def Lean.Grind.IntModule.OfNatModule.zsmul {α : Type u} [NatModule α] (n : Int) (q : Q α) :

Q α

Equations

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

Instances For

def Lean.Grind.IntModule.OfNatModule.sub {α : Type u} [NatModule α] (q₁ q₂ : Q α) :

Q α

Equations

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

Instances For

def Lean.Grind.IntModule.OfNatModule.add {α : Type u} [NatModule α] (q₁ q₂ : Q α) :

Q α

Equations

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

Instances For

def Lean.Grind.IntModule.OfNatModule.neg {α : Type u} [NatModule α] (q : Q α) :

Q α

Equations

Lean.Grind.IntModule.OfNatModule.neg q = Quot.liftOn q (fun (x : α × α) => match x with | (a, b) => Lean.Grind.IntModule.OfNatModule.Q.mk (b, a)) ⋯

Instances For

def Lean.Grind.IntModule.OfNatModule.zero {α : Type u} [NatModule α] :

Q α

Equations

Lean.Grind.IntModule.OfNatModule.zero = Lean.Grind.IntModule.OfNatModule.Q.mk (0, 0)

Instances For

theorem Lean.Grind.IntModule.OfNatModule.neg_add_cancel {α : Type u} [NatModule α] (a : Q α) :

add (neg a) a = zero

theorem Lean.Grind.IntModule.OfNatModule.add_comm {α : Type u} [NatModule α] (a b : Q α) :

add a b = add b a

theorem Lean.Grind.IntModule.OfNatModule.add_zero {α : Type u} [NatModule α] (a : Q α) :

theorem Lean.Grind.IntModule.OfNatModule.add_assoc {α : Type u} [NatModule α] (a b c : Q α) :

add (add a b) c = add a (add b c)

theorem Lean.Grind.IntModule.OfNatModule.sub_eq_add_neg {α : Type u} [NatModule α] (a b : Q α) :

sub a b = add a (neg b)

theorem Lean.Grind.IntModule.OfNatModule.one_zsmul {α : Type u} [NatModule α] (a : Q α) :

zsmul 1 a = a

theorem Lean.Grind.IntModule.OfNatModule.zero_zsmul {α : Type u} [NatModule α] (a : Q α) :

zsmul 0 a = zero

theorem Lean.Grind.IntModule.OfNatModule.add_zsmul {α : Type u} [NatModule α] (a b : Int) (c : Q α) :

zsmul (a + b) c = add (zsmul a c) (zsmul b c)

theorem Lean.Grind.IntModule.OfNatModule.zsmul_natCast_eq_nsmul {α : Type u} [NatModule α] (n : Nat) (a : Q α) :

zsmul (↑n) a = nsmul n a

instance Lean.Grind.IntModule.OfNatModule.ofNatModule {α : Type u} [NatModule α] :

IntModule (Q α)

Equations

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

def Lean.Grind.IntModule.OfNatModule.toQ {α : Type u} [NatModule α] (a : α) :

Q α

Equations

Lean.Grind.IntModule.OfNatModule.toQ a = Lean.Grind.IntModule.OfNatModule.Q.mk (a, 0)

Instances For

Embedding theorems

theorem Lean.Grind.IntModule.OfNatModule.toQ_add {α : Type u} [NatModule α] (a b : α) :

toQ (a + b) = toQ a + toQ b

theorem Lean.Grind.IntModule.OfNatModule.toQ_zero {α : Type u} [NatModule α] :

toQ 0 = 0

theorem Lean.Grind.IntModule.OfNatModule.toQ_smul {α : Type u} [NatModule α] (n : Nat) (a : α) :

toQ (n • a) = n • toQ a

Helper definitions and theorems for proving toQ is injective when CommSemiring has the right_cancel property

theorem Lean.Grind.IntModule.OfNatModule.Q.exact {α : Type u} [NatModule α] {a b : α × α} :

mk a = mk b → r α a b

theorem Lean.Grind.IntModule.OfNatModule.toQ_inj {α : Type u} [NatModule α] [AddRightCancel α] {a b : α} :

toQ a = toQ b → a = b

instance Lean.Grind.IntModule.OfNatModule.instNoNatZeroDivisorsQOfAddRightCancel {α : Type u} [NatModule α] [AddRightCancel α] [NoNatZeroDivisors α] :

NoNatZeroDivisors (Q α)

instance Lean.Grind.IntModule.OfNatModule.instLEQOfOrderedAdd {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :

LE (Q α)

Equations

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

instance Lean.Grind.IntModule.OfNatModule.instLTQOfOrderedAdd {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :

LT (Q α)

Equations

Lean.Grind.IntModule.OfNatModule.instLTQOfOrderedAdd = { lt := fun (a b : Lean.Grind.IntModule.OfNatModule.Q α) => a ≤ b ∧ ¬b ≤ a }

theorem Lean.Grind.IntModule.OfNatModule.mk_le_mk {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} :

Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁

instance Lean.Grind.IntModule.OfNatModule.instIsPreorderQ {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :

Std.IsPreorder (Q α)

instance Lean.Grind.IntModule.OfNatModule.instIsPartialOrderQ {α : Type u} [NatModule α] [LE α] [Std.IsPartialOrder α] [OrderedAdd α] :

Std.IsPartialOrder (Q α)

instance Lean.Grind.IntModule.OfNatModule.instIsLinearPreorderQ {α : Type u} [NatModule α] [LE α] [Std.IsLinearPreorder α] [OrderedAdd α] :

Std.IsLinearPreorder (Q α)

instance Lean.Grind.IntModule.OfNatModule.instIsLinearOrderQ {α : Type u} [NatModule α] [LE α] [Std.IsLinearOrder α] [OrderedAdd α] :

Std.IsLinearOrder (Q α)

theorem Lean.Grind.IntModule.OfNatModule.toQ_le {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} :

toQ a ≤ toQ b ↔ a ≤ b

theorem Lean.Grind.IntModule.OfNatModule.toQ_lt {α : Type u} [NatModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} :

toQ a < toQ b ↔ a < b

instance Lean.Grind.IntModule.OfNatModule.instOrderedAddQ {α : Type u} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] :

OrderedAdd (Q α)