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.

Instances For

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

    Instances For
      theorem Mathlib.Meta.NormNum.isNat_ofNat (α : Type u_1) [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.

        Instances For

          Casts #

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

          Instances For

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

            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'Nat.add a' 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'Int.add a' 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.

              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.

                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 dbInt.add (Int.mul na db) (Int.mul nb da) = Int.mul (k) ncNat.mul da db = Nat.mul k 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.

                  Instances For
                    theorem Mathlib.Meta.NormNum.isInt_neg {α : Type u_1} [Ring α] {f : αα} {a : α} {a' : } {b : } :
                    f = Neg.negMathlib.Meta.NormNum.IsInt a a'Int.neg a' = 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 dInt.neg n = 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.

                    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'Int.sub a' 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₁ : Int.sub (Int.mul na db) (Int.mul nb da) = Int.mul (k) nc) (h₂ : Nat.mul da db = Nat.mul k 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.

                      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'Nat.mul a' 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'Int.mul a' 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 dbInt.mul na nb = Int.mul (k) ncNat.mul da db = Nat.mul k 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.

                        Instances For
                          theorem Mathlib.Meta.NormNum.isRat_div {α : Type u_1} [DivisionRing α] {a : α} {b : α} {cn : } {cd : } :

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

                          Instances For

                            Logic #

                            The norm_num extension which identifies True.

                            Instances For

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

                              Instances For

                                (In)equalities #

                                theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u_1} [Ring α] {a : α} {b : α} {z : } :
                                theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u_1} [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.

                                Instances For

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

                                  Instances For

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

                                    Instances For

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

                                      Instances For