Documentation

Mathlib.Tactic.NormNum.Inv

norm_num plugins for Rat.cast and ⁻¹. #

source
theorem Mathlib.Meta.NormNum.isRat_mkRat {a : ℤ} {na : ℤ} {n : ℤ} {b : ℕ} {nb : ℕ} {d : ℕ} :
Mathlib.Meta.NormNum.IsInt a na → Mathlib.Meta.NormNum.IsNat b nb → Mathlib.Meta.NormNum.IsRat (↑na / ↑nb) n d → Mathlib.Meta.NormNum.IsRat (mkRat a b) n d
source
def Mathlib.Meta.NormNum.evalMkRat :
Mathlib.Meta.NormNum.NormNumExt

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

Instances For
    source
    theorem Mathlib.Meta.NormNum.isNat_ratCast {R : Type u_1} [DivisionRing R] {q : ℚ} {n : ℕ} :
    Mathlib.Meta.NormNum.IsNat q n → Mathlib.Meta.NormNum.IsNat (↑q) n
    source
    theorem Mathlib.Meta.NormNum.isInt_ratCast {R : Type u_1} [DivisionRing R] {q : ℚ} {n : ℤ} :
    Mathlib.Meta.NormNum.IsInt q n → Mathlib.Meta.NormNum.IsInt (↑q) n
    source
    theorem Mathlib.Meta.NormNum.isRat_ratCast {R : Type u_1} [DivisionRing R] [CharZero R] {q : ℚ} {n : ℤ} {d : ℕ} :
    Mathlib.Meta.NormNum.IsRat q n d → Mathlib.Meta.NormNum.IsRat (↑q) n d
    source
    def Mathlib.Meta.NormNum.evalRatCast :
    Mathlib.Meta.NormNum.NormNumExt

    The norm_num extension which identifies an expression RatCast.ratCast q where norm_num recognizes q, returning the cast of q.

    Instances For
      source
      theorem Mathlib.Meta.NormNum.isRat_inv_pos {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n : ℕ} {d : ℕ} :
      Mathlib.Meta.NormNum.IsRat a (Int.ofNat (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)
      source
      theorem Mathlib.Meta.NormNum.isRat_inv_one {α : Type u_1} [DivisionRing α] {a : α} :
      Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a⁻¹ 1
      source
      theorem Mathlib.Meta.NormNum.isRat_inv_zero {α : Type u_1} [DivisionRing α] {a : α} :
      Mathlib.Meta.NormNum.IsNat a 0 → Mathlib.Meta.NormNum.IsNat a⁻¹ 0
      source
      theorem Mathlib.Meta.NormNum.isRat_inv_neg_one {α : Type u_1} [DivisionRing α] {a : α} :
      Mathlib.Meta.NormNum.IsInt a (Int.negOfNat 1) → Mathlib.Meta.NormNum.IsInt a⁻¹ (Int.negOfNat 1)
      source
      theorem Mathlib.Meta.NormNum.isRat_inv_neg {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n : ℕ} {d : ℕ} :
      Mathlib.Meta.NormNum.IsRat a (Int.negOfNat (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)
      source
      def Mathlib.Meta.NormNum.evalInv :
      Mathlib.Meta.NormNum.NormNumExt

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

      Instances For