Commit 2025-08-13 09:12 69035af7

View on Github →

refactor: Add norm_num machinery for NNRat (#9915) This splits the previous isRat primitive into isNNRat and isNegNNRat, where only the latter carries around a DivisionRing instance. This means that norm_num works on NNReal and NNRat.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added theorem Mathlib.Meta.Positivity.log_nz_of_isNNRat

deleted theorem Mathlib.Meta.Positivity.log_nz_of_isRat

added theorem Mathlib.Meta.Positivity.log_pos_of_isNNRat

deleted theorem Mathlib.Meta.Positivity.log_pos_of_isRat

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Mathlib.Meta.NormNum.isNNRat_rpow_neg

added theorem Mathlib.Meta.NormNum.isNNRat_rpow_pos

Modified Mathlib/Data/Rat/Floor.lean

deleted theorem Rat.isInt_intCeil_ofIsRat

added theorem Rat.isInt_intCeil_ofIsRat_neg

deleted theorem Rat.isInt_intFloor_ofIsRat

added theorem Rat.isInt_intFloor_ofIsRat_neg

added theorem Rat.isNat_intCeil_ofIsNNRat

added theorem Rat.isNat_intFloor_ofIsNNRat

Modified Mathlib/Tactic/NormNum/Basic.lean

added def Mathlib.Meta.NormNum.inferDivisionSemiring

added theorem Mathlib.Meta.NormNum.isNNRat_add

added theorem Mathlib.Meta.NormNum.isNNRat_div

added theorem Mathlib.Meta.NormNum.isNNRat_eq_true

added theorem Mathlib.Meta.NormNum.isNNRat_mul

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified Mathlib/Tactic/NormNum/Eq.lean

added theorem Mathlib.Meta.NormNum.NNRat.invOf_denom_swap

added theorem Mathlib.Meta.NormNum.isNNRat_eq_false

Modified Mathlib/Tactic/NormNum/Ineq.lean

added def Mathlib.Meta.NormNum.inferLinearOrderedSemifield

added theorem Mathlib.Meta.NormNum.isNNRat_le_false

added theorem Mathlib.Meta.NormNum.isNNRat_le_true

added theorem Mathlib.Meta.NormNum.isNNRat_lt_false

added theorem Mathlib.Meta.NormNum.isNNRat_lt_true

Modified Mathlib/Tactic/NormNum/Inv.lean

added def Mathlib.Meta.NormNum.inferCharZeroOfDivisionSemiring?

added theorem Mathlib.Meta.NormNum.isInt_inv_neg_one

added theorem Mathlib.Meta.NormNum.isNNRat_inv_pos

added theorem Mathlib.Meta.NormNum.isNNRat_ratCast

added theorem Mathlib.Meta.NormNum.isNat_inv_one

added theorem Mathlib.Meta.NormNum.isNat_inv_zero

deleted theorem Mathlib.Meta.NormNum.isRat_inv_neg_one

deleted theorem Mathlib.Meta.NormNum.isRat_inv_one

deleted theorem Mathlib.Meta.NormNum.isRat_inv_zero

Modified Mathlib/Tactic/NormNum/Irrational.lean

Modified Mathlib/Tactic/NormNum/OfScientific.lean

added theorem Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true

deleted theorem Mathlib.Meta.NormNum.isRat_ofScientific_of_true

Modified Mathlib/Tactic/NormNum/Pow.lean

added theorem Mathlib.Meta.NormNum.isNNRat_pow

added theorem Mathlib.Meta.NormNum.isNNRat_zpow_neg

added theorem Mathlib.Meta.NormNum.isNNRat_zpow_pos

Modified Mathlib/Tactic/NormNum/RealSqrt.lean

added theorem Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat

added theorem Tactic.NormNum.isNNRat_realSqrt_of_isNNRat

deleted theorem Tactic.NormNum.isRat_realSqrt_of_isRat_ofNat

Modified Mathlib/Tactic/NormNum/Result.lean

added theorem Mathlib.Meta.NormNum.IsNNRat.den_nz

added theorem Mathlib.Meta.NormNum.IsNNRat.of_raw

added theorem Mathlib.Meta.NormNum.IsNNRat.to_eq

added theorem Mathlib.Meta.NormNum.IsNNRat.to_isNat

added theorem Mathlib.Meta.NormNum.IsNNRat.to_isRat

added theorem Mathlib.Meta.NormNum.IsNNRat.to_raw_eq

added inductive Mathlib.Meta.NormNum.IsNNRat

added theorem Mathlib.Meta.NormNum.IsNat.to_isNNRat

deleted theorem Mathlib.Meta.NormNum.IsNat.to_isRat

deleted theorem Mathlib.Meta.NormNum.IsRat.nonneg_to_eq

added theorem Mathlib.Meta.NormNum.IsRat.to_isNNRat

deleted theorem Mathlib.Meta.NormNum.IsRat.to_isNat

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

added def Mathlib.Meta.NormNum.Result.isNNRat

added def Mathlib.Meta.NormNum.Result.isNegNNRat

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

modified def Mathlib.Meta.NormNum.Result.isRat

added def Mathlib.Meta.NormNum.Result.ofRawNNRat

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

added def Mathlib.Meta.NormNum.instAddMonoidWithOne'

added def NNRat.rawCast

Modified Mathlib/Tactic/Positivity/Core.lean

added theorem Mathlib.Meta.Positivity.nonneg_of_isNNRat

added theorem Mathlib.Meta.Positivity.pos_of_isNNRat

Modified Mathlib/Tactic/Ring/Basic.lean

added def Mathlib.Tactic.Ring.ExProd.mkNNRat

added def Mathlib.Tactic.Ring.ExProd.mkNegNNRat

deleted def Mathlib.Tactic.Ring.ExProd.mkRat

added theorem Mathlib.Tactic.Ring.cast_nnrat

Modified Mathlib/Tactic/Ring/RingNF.lean

added theorem Mathlib.Tactic.RingNF.nnrat_rawCast

deleted theorem Mathlib.Tactic.RingNF.rat_rawCast_pos

Modified MathlibTest/norm_num.lean

Modified MathlibTest/norm_num_ext.lean

Modified MathlibTest/ring.lean

Modified scripts/nolints.json