Commit 2025-02-13 18:08 5c5692ed

View on Github →

chore: reduce imports of Algebra.Order.Floor (#21805)

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Data/Int/Cast/Basic.lean

added theorem Int.toNat_of_nonpos

Modified Mathlib/Data/Int/Lemmas.lean

deleted theorem Int.toNat_of_nonpos