Commit 2023-01-27 15:48 8e2f0beb

View on Github →

feat: Rat functionality for ring (#1711) We implement #1189.

Estimated changes

Modified Mathlib/Algebra/Field/Basic.lean

added theorem inv_neg_one

Modified Mathlib/Tactic/NormNum/Basic.lean

added theorem Mathlib.Meta.NormNum.isRat_inv_neg_one

added theorem Mathlib.Meta.NormNum.isRat_inv_one

Modified Mathlib/Tactic/NormNum/Core.lean

added def Lean.LOption.toOption

added theorem Mathlib.Meta.NormNum.IsRat.den_nz

added theorem Mathlib.Meta.NormNum.IsRat.of_raw

deleted def Mathlib.Meta.NormNum.Rat.rawCast

added def Mathlib.Meta.NormNum.Result.ofRawRat

added def Mathlib.Meta.NormNum.Result.toRatNZ

added def Rat.rawCast

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Tactic/Ring/Basic.lean

deleted def Lean.LOption.toOption

modified def Mathlib.Tactic.Ring.Cache.nat

modified structure Mathlib.Tactic.Ring.Cache

modified def Mathlib.Tactic.Ring.ExProd.coeff

added def Mathlib.Tactic.Ring.ExProd.evalInv

added def Mathlib.Tactic.Ring.ExProd.mkRat

added def Mathlib.Tactic.Ring.ExSum.evalInv

added theorem Mathlib.Tactic.Ring.cast_rat

added theorem Mathlib.Tactic.Ring.div_congr

added theorem Mathlib.Tactic.Ring.div_pf

added def Mathlib.Tactic.Ring.evalDiv

added def Mathlib.Tactic.Ring.evalInvAtom

added theorem Mathlib.Tactic.Ring.inv_add

added theorem Mathlib.Tactic.Ring.inv_congr

added theorem Mathlib.Tactic.Ring.inv_mul

added theorem Mathlib.Tactic.Ring.inv_single

added def Mathlib.Tactic.Ring.mkCache

added theorem Mathlib.Tactic.Ring.natCast_add

added theorem Mathlib.Tactic.Ring.natCast_mul

added theorem Mathlib.Tactic.Ring.natCast_nat

added theorem Mathlib.Tactic.Ring.natCast_zero

deleted theorem Mathlib.Tactic.Ring.nat_cast_add

deleted theorem Mathlib.Tactic.Ring.nat_cast_mul

deleted theorem Mathlib.Tactic.Ring.nat_cast_nat

deleted theorem Mathlib.Tactic.Ring.nat_cast_zero

added theorem Mathlib.Tactic.Ring.toProd_pf

Modified Mathlib/Tactic/Ring/RingNF.lean

added theorem Mathlib.Tactic.RingNF.rat_rawCast_2

Modified test/linarith.lean

Modified test/norm_num.lean

Modified test/ring.lean