Documentation

Init.Grind.Module.Envelope

def Lean.Grind.IntModule.OfNatModule.r (α : Type u) [NatModule α] :
α × αα × αProp
Equations
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 br α b a
    theorem Lean.Grind.IntModule.OfNatModule.r_trans {α : Type u} [NatModule α] {a b c : α × α} :
    r α a br α b cr α a c
    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
    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.hmulNat {α : Type u} [NatModule α] (n : Nat) (q : Q α) :
        Q α
        Equations
        Instances For
          def Lean.Grind.IntModule.OfNatModule.hmulInt {α : 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
                Instances For
                  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_assoc {α : Type u} [NatModule α] (a b c : Q α) :
                  add (add a b) c = add a (add b c)
                  theorem Lean.Grind.IntModule.OfNatModule.hmul_add {α : Type u} [NatModule α] (a : Int) (b c : Q α) :
                  hmulInt a (add b c) = add (hmulInt a b) (hmulInt a c)
                  theorem Lean.Grind.IntModule.OfNatModule.add_hmul {α : Type u} [NatModule α] (a b : Int) (c : Q α) :
                  hmulInt (a + b) c = add (hmulInt a c) (hmulInt b c)
                  theorem Lean.Grind.IntModule.OfNatModule.hmul_nat {α : Type u} [NatModule α] (n : Nat) (a : Q α) :
                  hmulInt (↑n) a = hmulNat n a
                  Equations
                  • One or more equations did not get rendered due to their size.

                  Embedding theorems

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

                  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 br α a b
                  theorem Lean.Grind.IntModule.OfNatModule.toQ_inj {α : Type u} [NatModule α] [AddRightCancel α] {a b : α} :
                  toQ a = toQ ba = b
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem Lean.Grind.IntModule.OfNatModule.mk_le_mk {α : Type u} [NatModule α] [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} :
                  Q.mk (a₁, a₂) Q.mk (b₁, b₂) a₁ + b₂ a₂ + b₁
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem Lean.Grind.IntModule.OfNatModule.toQ_le {α : Type u} [NatModule α] [Preorder α] [OrderedAdd α] {a b : α} :
                  toQ a toQ b a b
                  theorem Lean.Grind.IntModule.OfNatModule.toQ_lt {α : Type u} [NatModule α] [Preorder α] [OrderedAdd α] {a b : α} :
                  toQ a < toQ b a < b