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
Instances For
Equations
Instances For
Equations
- Lean.Grind.IntModule.OfNatModule.hmulNat n q = Quot.liftOn q (fun (x : α × α) => match x with | (a, b) => Lean.Grind.IntModule.OfNatModule.Q.mk (n * a, n * b)) ⋯
Instances For
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
Instances For
Instances For
Embedding theorems
Helper definitions and theorems for proving toQ
is injective when
CommSemiring
has the right_cancel property
theorem
Lean.Grind.IntModule.OfNatModule.toQ_inj
{α : Type u}
[NatModule α]
[AddRightCancel α]
{a b : α}
:
instance
Lean.Grind.IntModule.OfNatModule.instNoNatZeroDivisorsQOfAddRightCancel
{α : Type u}
[NatModule α]
[AddRightCancel α]
[NoNatZeroDivisors α]
:
NoNatZeroDivisors (Q α)
instance
Lean.Grind.IntModule.OfNatModule.instLEQOfOrderedAdd
{α : Type u}
[NatModule α]
[Preorder α]
[OrderedAdd α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Grind.IntModule.OfNatModule.instPreorderQOfOrderedAdd
{α : Type u}
[NatModule α]
[Preorder α]
[OrderedAdd α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Grind.IntModule.OfNatModule.instOrderedAddQ
{α : Type u}
[NatModule α]
[Preorder α]
[OrderedAdd α]
:
OrderedAdd (Q α)