norm_num plugins for Rat.cast and ⁻¹.

def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : Q(Type u)} (_i : autoParam Q(Ring «$α») _auto✝) : Lean.MetaM Q(CharZero «$α»)

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

Equations

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

def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : Q(Type u)} (_i : autoParam Q(Ring «$α») _auto✝) : Lean.MetaM (Option Q(CharZero «$α»))

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

Equations

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

def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne {u : Lean.Level} {α : Q(Type u)} (_i : autoParam Q(AddMonoidWithOne «$α») _auto✝) : 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 : autoParam Q(AddMonoidWithOne «$α») _auto✝) : Lean.MetaM (Option Q(CharZero «$α»))

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

Equations

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

def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : Q(Type u)} (_i : autoParam Q(DivisionRing «$α») _auto✝) : 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 : autoParam Q(DivisionRing «$α») _auto✝) : Lean.MetaM (Option Q(CharZero «$α»))

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

Equations

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

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 (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)

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 (Nat.succ n)) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)

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 : Q(«$α»)) (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.

Equations

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