norm_num plugins for Rat.cast and ⁻¹.

def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : Q(Type u)} (_i : Q(Ring «$α») := by with_reducible assumption) : Lean.MetaM Q(CharZero «$α»)

Helper function to synthesize a typed CharZero α expression given Ring α.

Equations

• Mathlib.Meta.NormNum.inferCharZeroOfRing _i = do let __do_lift ← Qq.synthInstanceQ q(CharZero «$α») <|> Lean.throwError (Lean.toMessageData "not a characteristic zero ring") pure __do_lift

def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : Q(Type u)} (_i : Q(Ring «$α») := by with_reducible assumption) : Lean.MetaM (Option Q(CharZero «$α»))

Helper function to synthesize a typed CharZero α expression given Ring α, if it exists.

Equations

• Mathlib.Meta.NormNum.inferCharZeroOfRing? _i = do let __do_lift ← Qq.trySynthInstanceQ q(CharZero «$α») pure __do_lift.toOption

def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne {u : Lean.Level} {α : Q(Type u)} (_i : Q(AddMonoidWithOne «$α») := by with_reducible assumption) : Lean.MetaM Q(CharZero «$α»)

Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

Equations

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

def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne? {u : Lean.Level} {α : Q(Type u)} (_i : Q(AddMonoidWithOne «$α») := by with_reducible assumption) : Lean.MetaM (Option Q(CharZero «$α»))

Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α, if it exists.

Equations

• Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne? _i = do let __do_lift ← Qq.trySynthInstanceQ q(CharZero «$α») pure __do_lift.toOption

def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : Q(Type u)} (_i : Q(DivisionRing «$α») := by with_reducible assumption) : Lean.MetaM Q(CharZero «$α»)

Helper function to synthesize a typed CharZero α expression given DivisionRing α.

Equations

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

def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? {u : Lean.Level} {α : Q(Type u)} (_i : Q(DivisionRing «$α») := by with_reducible assumption) : Lean.MetaM (Option Q(CharZero «$α»))

Helper function to synthesize a typed CharZero α expression given DivisionRing α, if it exists.

Equations

• Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? _i = do let __do_lift ← Qq.trySynthInstanceQ q(CharZero «$α») pure __do_lift.toOption

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

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.

Equations

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

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

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

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

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.

Equations

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

theorem Mathlib.Meta.NormNum.isRat_inv_pos {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} : Mathlib.Meta.NormNum.IsRat a (Int.ofNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) n.succ

theorem Mathlib.Meta.NormNum.isRat_inv_one {α : Type u_1} [DivisionRing α] {a : α} : Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a⁻¹ 1

theorem Mathlib.Meta.NormNum.isRat_inv_zero {α : Type u_1} [DivisionRing α] {a : α} : Mathlib.Meta.NormNum.IsNat a 0 → Mathlib.Meta.NormNum.IsNat a⁻¹ 0

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)

theorem Mathlib.Meta.NormNum.isRat_inv_neg {α : Type u_1} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} : Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) n.succ

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.

Equations

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

def Mathlib.Meta.NormNum.evalInv.core {u : Lean.Level} {α : Q(Type u)} (e a : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (dα : Q(DivisionRing «$α»)) (i : Option Q(CharZero «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

Main part of evalInv.