Commit 2024-02-22 14:01 72c702f6

View on Github →

feat: positivity extension for Rat.num, Rat.den (#10218) and rename num_nonneg_iff_zero_le to num_nonneg, num_pos_iff_pos to num_pos From LeanAPAP

Estimated changes

Modified Archive/Imo/Imo2013Q5.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/NNRat/Lemmas.lean

Modified Mathlib/Data/Rat/Cast/Order.lean

Modified Mathlib/Data/Rat/Floor.lean

Modified Mathlib/Data/Rat/Order.lean

added theorem Rat.num_nonneg

deleted theorem Rat.num_nonneg_iff_zero_le

added theorem Rat.num_pos

deleted theorem Rat.num_pos_iff_pos

Modified Mathlib/Data/Rat/Star.lean

Modified Mathlib/NumberTheory/FLT/Basic.lean

Modified Mathlib/NumberTheory/Liouville/LiouvilleWith.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

added def Mathlib.Meta.Positivity.evalRatDen

added def Mathlib.Meta.Positivity.evalRatNum

Modified test/linarith.lean

Modified test/positivity.lean