Commit 2025-11-11 22:41 2ab6d475

View on Github →

feat: one-sided version of Int.cast_nonneg (#31477) ... which works for the zero ring also. This is especially useful for use in simp.

Estimated changes

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

Modified Mathlib/Algebra/Order/Ring/Cast.lean

modified theorem Int.cast_nonneg

added theorem Int.cast_nonneg_iff

Modified Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/NumberTheory/Real/Irrational.lean

Modified Mathlib/NumberTheory/Zsqrtd/ToReal.lean

Modified Mathlib/Tactic/Positivity/Basic.lean