Documentation

Mathlib.Tactic.NormNum.Basic

norm_num basic plugins #

This file adds norm_num plugins for

See other files in this directory for many more plugins.

Constructors and constants #

The norm_num extension which identifies the expression Zero.zero, returning 0.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The norm_num extension which identifies the expression One.one, returning 1.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Mathlib.Meta.NormNum.isNat_ofNat (α : Type u) [AddMonoidWithOne α] {a : α} {n : } (h : n = a) :

      The norm_num extension which identifies an expression OfNat.ofNat n, returning n.

      Instances For

        The norm_num extension which identifies the constructor application Int.ofNat n such that norm_num successfully recognizes n, returning n.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The norm_num extension which identifies the expression Int.natAbs n such that norm_num successfully recognizes n.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Casts #

            @[deprecated Mathlib.Meta.NormNum.isNat_natCast]

            Alias of Mathlib.Meta.NormNum.isNat_natCast.

            The norm_num extension which identifies an expression Nat.cast n, returning n.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[deprecated Mathlib.Meta.NormNum.isNat_intCast]

              Alias of Mathlib.Meta.NormNum.isNat_intCast.

              @[deprecated Mathlib.Meta.NormNum.isintCast]

              Alias of Mathlib.Meta.NormNum.isintCast.

              The norm_num extension which identifies an expression Int.cast n, returning n.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Arithmetic #

                theorem Mathlib.Meta.NormNum.isNat_add {α : Type u_1} [AddMonoidWithOne α] {f : ααα} {a : α} {b : α} {a' : } {b' : } {c : } :
                f = HAdd.hAddMathlib.Meta.NormNum.IsNat a a'Mathlib.Meta.NormNum.IsNat b b'a'.add b' = cMathlib.Meta.NormNum.IsNat (f a b) c
                theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {a' : } {b' : } {c : } :
                f = HAdd.hAddMathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsInt b b'a'.add b' = cMathlib.Meta.NormNum.IsInt (f a b) c
                def Mathlib.Meta.NormNum.invertibleOfMul {α : Type u_1} [Semiring α] (k : ) (b : α) (a : α) [Invertible a] :
                a = k * bInvertible b

                If b divides a and a is invertible, then b is invertible.

                Equations
                Instances For
                  def Mathlib.Meta.NormNum.invertibleOfMul' {α : Type u_1} [Semiring α] {a : } {k : } {b : } [Invertible a] (h : a = k * b) :

                  If b divides a and a is invertible, then b is invertible.

                  Equations
                  Instances For
                    theorem Mathlib.Meta.NormNum.isRat_add {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {na : } {nb : } {nc : } {da : } {db : } {dc : } {k : } :
                    f = HAdd.hAddMathlib.Meta.NormNum.IsRat a na daMathlib.Meta.NormNum.IsRat b nb db(na.mul db).add (nb.mul da) = (↑k).mul ncda.mul db = k.mul dcMathlib.Meta.NormNum.IsRat (f a b) nc dc

                    Consider an Option as an object in the MetaM monad, by throwing an error on none.

                    Equations
                    Instances For

                      The norm_num extension which identifies expressions of the form a + b, such that norm_num successfully recognises both a and b.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Mathlib.Meta.NormNum.evalAdd.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

                        Main part of evalAdd.

                        Instances For
                          def Mathlib.Meta.NormNum.evalAdd.core.intArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Mathlib.Meta.NormNum.evalAdd.core.ratArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Mathlib.Meta.NormNum.isInt_neg {α : Type u_1} [Ring α] {f : αα} {a : α} {a' : } {b : } :
                              f = Neg.negMathlib.Meta.NormNum.IsInt a a'a'.neg = bMathlib.Meta.NormNum.IsInt (-a) b
                              theorem Mathlib.Meta.NormNum.isRat_neg {α : Type u_1} [Ring α] {f : αα} {a : α} {n : } {n' : } {d : } :
                              f = Neg.negMathlib.Meta.NormNum.IsRat a n dn.neg = n'Mathlib.Meta.NormNum.IsRat (-a) n' d

                              The norm_num extension which identifies expressions of the form -a, such that norm_num successfully recognises a.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Mathlib.Meta.NormNum.evalNeg.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»)) (a : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rα : Q(Ring «$α»)) :

                                Main part of evalNeg.

                                Equations
                                Instances For
                                  theorem Mathlib.Meta.NormNum.isInt_sub {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {a' : } {b' : } {c : } :
                                  f = HSub.hSubMathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsInt b b'a'.sub b' = cMathlib.Meta.NormNum.IsInt (f a b) c
                                  theorem Mathlib.Meta.NormNum.isRat_sub {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {na : } {nb : } {nc : } {da : } {db : } {dc : } {k : } (hf : f = HSub.hSub) (ra : Mathlib.Meta.NormNum.IsRat a na da) (rb : Mathlib.Meta.NormNum.IsRat b nb db) (h₁ : (na.mul db).sub (nb.mul da) = (↑k).mul nc) (h₂ : da.mul db = k.mul dc) :

                                  The norm_num extension which identifies expressions of the form a - b in a ring, such that norm_num successfully recognises both a and b.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Mathlib.Meta.NormNum.evalSub.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (rα : Q(Ring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

                                    Main part of evalAdd.

                                    Instances For
                                      theorem Mathlib.Meta.NormNum.isNat_mul {α : Type u_1} [Semiring α] {f : ααα} {a : α} {b : α} {a' : } {b' : } {c : } :
                                      f = HMul.hMulMathlib.Meta.NormNum.IsNat a a'Mathlib.Meta.NormNum.IsNat b b'a'.mul b' = cMathlib.Meta.NormNum.IsNat (a * b) c
                                      theorem Mathlib.Meta.NormNum.isInt_mul {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {a' : } {b' : } {c : } :
                                      f = HMul.hMulMathlib.Meta.NormNum.IsInt a a'Mathlib.Meta.NormNum.IsInt b b'a'.mul b' = cMathlib.Meta.NormNum.IsInt (a * b) c
                                      theorem Mathlib.Meta.NormNum.isRat_mul {α : Type u_1} [Ring α] {f : ααα} {a : α} {b : α} {na : } {nb : } {nc : } {da : } {db : } {dc : } {k : } :
                                      f = HMul.hMulMathlib.Meta.NormNum.IsRat a na daMathlib.Meta.NormNum.IsRat b nb dbna.mul nb = (↑k).mul ncda.mul db = k.mul dcMathlib.Meta.NormNum.IsRat (f a b) nc dc

                                      The norm_num extension which identifies expressions of the form a * b, such that norm_num successfully recognises both a and b.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def Mathlib.Meta.NormNum.evalMul.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) :

                                        Main part of evalMul.

                                        Instances For
                                          def Mathlib.Meta.NormNum.evalMul.core.intArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) :
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def Mathlib.Meta.NormNum.evalMul.core.ratArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α»«$α»«$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) :
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem Mathlib.Meta.NormNum.isRat_div {α : Type u} [DivisionRing α] {a : α} {b : α} {cn : } {cd : } :

                                              Helper function to synthesize a typed DivisionRing α expression.

                                              Equations
                                              Instances For

                                                The norm_num extension which identifies expressions of the form a / b, such that norm_num successfully recognises both a and b.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Logic #

                                                  The norm_num extension which identifies True.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    The norm_num extension which identifies False.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      The norm_num extension which identifies expressions of the form ¬a, such that norm_num successfully recognises a.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        (In)equalities #

                                                        theorem Mathlib.Meta.NormNum.ble_eq_false {x : } {y : } :
                                                        x.ble y = false y < x
                                                        theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u} [Ring α] {a : α} {b : α} {z : } :
                                                        theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u} [Ring α] {a : α} {b : α} {n : } {d : } :
                                                        theorem Mathlib.Meta.NormNum.eq_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :
                                                        a = b
                                                        theorem Mathlib.Meta.NormNum.ne_of_false_of_true {a : Prop} {b : Prop} (ha : ¬a) (hb : b) :
                                                        a b
                                                        theorem Mathlib.Meta.NormNum.ne_of_true_of_false {a : Prop} {b : Prop} (ha : a) (hb : ¬b) :
                                                        a b
                                                        theorem Mathlib.Meta.NormNum.eq_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
                                                        a = b

                                                        Nat operations #

                                                        The norm_num extension which identifies expressions of the form Nat.succ a, such that norm_num successfully recognises a.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Mathlib.Meta.NormNum.isNat_natSub {a : } {b : } {a' : } {b' : } {c : } :

                                                          The norm_num extension which identifies expressions of the form Nat.sub a b, such that norm_num successfully recognises both a and b.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            theorem Mathlib.Meta.NormNum.isNat_natMod {a : } {b : } {a' : } {b' : } {c : } :

                                                            The norm_num extension which identifies expressions of the form Nat.mod a b, such that norm_num successfully recognises both a and b.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              theorem Mathlib.Meta.NormNum.isNat_natDiv {a : } {b : } {a' : } {b' : } {c : } :

                                                              The norm_num extension which identifies expressions of the form Nat.div a b, such that norm_num successfully recognises both a and b.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem Mathlib.Meta.NormNum.isNat_dvd_true {a : } {b : } {a' : } {b' : } :
                                                                Mathlib.Meta.NormNum.IsNat a a'Mathlib.Meta.NormNum.IsNat b b'b'.mod a' = 0a b
                                                                theorem Mathlib.Meta.NormNum.isNat_dvd_false {a : } {b : } {a' : } {b' : } {c : } :
                                                                Mathlib.Meta.NormNum.IsNat a a'Mathlib.Meta.NormNum.IsNat b b'b'.mod a' = c.succ¬a b

                                                                The norm_num extension which identifies expressions of the form (a : ℕ) | b, such that norm_num successfully recognises both a and b.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For