Commit 2023-01-14 01:39 3aaa8a54

View on Github →

feat: Rat-dependent norm_num functionality (#1441) As per #1102, we extend norm_num to handle Rats. We leave most of the theorems sorried, but the evaluation and tests work!

Estimated changes

Modified Mathlib/Algebra/Invertible.lean

added theorem Invertible.cong

added theorem invOf_one'

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

added def Mathlib.Meta.NormNum.evalDiv

added def Mathlib.Meta.NormNum.evalInv

added theorem Mathlib.Meta.NormNum.isRat_add

added theorem Mathlib.Meta.NormNum.isRat_div

added theorem Mathlib.Meta.NormNum.isRat_inv_neg

added theorem Mathlib.Meta.NormNum.isRat_inv_pos

added theorem Mathlib.Meta.NormNum.isRat_inv_zero

added theorem Mathlib.Meta.NormNum.isRat_mul

added theorem Mathlib.Meta.NormNum.isRat_neg

added theorem Mathlib.Meta.NormNum.isRat_pow

added theorem Mathlib.Meta.NormNum.isRat_sub

Modified Mathlib/Tactic/NormNum/Core.lean

added theorem Mathlib.Meta.NormNum.IsInt.to_isRat

added theorem Mathlib.Meta.NormNum.IsNat.to_isRat

added theorem Mathlib.Meta.NormNum.IsRat.neg_to_eq

added theorem Mathlib.Meta.NormNum.IsRat.nonneg_to_eq

added theorem Mathlib.Meta.NormNum.IsRat.of_raw

added theorem Mathlib.Meta.NormNum.IsRat.to_isInt

added theorem Mathlib.Meta.NormNum.IsRat.to_isNat

added theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq

added inductive Mathlib.Meta.NormNum.IsRat

deleted structure Mathlib.Meta.NormNum.IsRat

added def Mathlib.Meta.NormNum.Rat.rawCast

modified def Mathlib.Meta.NormNum.Result.isInt

added def Mathlib.Meta.NormNum.Result.isRat'

added def Mathlib.Meta.NormNum.Result.ofRawRat

added def Mathlib.Meta.NormNum.Result.toRat'

modified def Mathlib.Meta.NormNum.Result.toRawEq

added def Mathlib.Meta.NormNum.Result.toRawIntEq

added def Mathlib.Meta.NormNum.deriveRat

added def Mathlib.Meta.NormNum.inferDivisionRing

added def Mathlib.Meta.NormNum.instDivisionRingRat

added def Mathlib.Meta.NormNum.instRingRat

modified def Mathlib.Meta.NormNum.isRatLit

added def Mathlib.Meta.NormNum.mkRawRatLit

Modified Mathlib/Tactic/Ring/Basic.lean

Modified test/linear_combination.lean

Modified test/norm_num.lean