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.inferCharZeroOfDivisionSemiring? {u : Lean.Level} {α : Q(Type u)} (_i : Q(DivisionSemiring «$α») := by with_reducible assumption) : Lean.MetaM (Option Q(CharZero «$α»))

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

Equations

• Mathlib.Meta.NormNum.inferCharZeroOfDivisionSemiring? _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 (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 : ℕ} : IsInt a na → IsNat b nb → IsRat (↑na / ↑nb) n d → IsRat (mkRat a b) n d

def Mathlib.Meta.NormNum.evalMkRat : 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 : ℕ} : IsNat q n → IsNat (↑q) n

theorem Mathlib.Meta.NormNum.isInt_ratCast {R : Type u_1} [DivisionRing R] {q : ℚ} {n : ℤ} : IsInt q n → IsInt (↑q) n

theorem Mathlib.Meta.NormNum.isNNRat_ratCast {R : Type u_1} [DivisionRing R] [CharZero R] {q : ℚ} {n d : ℕ} : IsNNRat q n d → IsNNRat (↑q) n d

theorem Mathlib.Meta.NormNum.isRat_ratCast {R : Type u_1} [DivisionRing R] [CharZero R] {q : ℚ} {n : ℤ} {d : ℕ} : IsRat q n d → IsRat (↑q) n d

def Mathlib.Meta.NormNum.evalRatCast : 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.isNNRat_inv_pos {α : Type u_1} [DivisionSemiring α] [CharZero α] {a : α} {n d : ℕ} : IsNNRat a n.succ d → IsNNRat a⁻¹ d n.succ

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

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

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

theorem Mathlib.Meta.NormNum.isInt_inv_neg_one {α : Type u_1} [DivisionRing α] {a : α} : IsInt a (Int.negOfNat 1) → IsInt a⁻¹ (Int.negOfNat 1)

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

def Mathlib.Meta.NormNum.evalInv : 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 : Result a) (dsα : Q(DivisionSemiring «$α»)) (i : Option Q(CharZero «$α»)) : Lean.MetaM (Result e)

Main part of evalInv.

Equations

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