Commit 2025-01-16 10:39 b73051c1

View on Github →

feat: split Mathlib/Algebra/Order/Ring/Unbundled/Nonneg (#20703) Motivated by the longest pole.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/GroupWithZero/Bounds.lean

added theorem BddAbove.range_comp_of_nonneg

added theorem bddAbove_range_mul

Renamed Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean to Mathlib/Algebra/Order/Nonneg/Basic.lean

deleted theorem BddAbove.range_comp_of_nonneg

deleted theorem Nonneg.bot_eq

deleted theorem bddAbove_range_mul

Modified Mathlib/Algebra/Order/Nonneg/Floor.lean

Created Mathlib/Algebra/Order/Nonneg/Lattice.lean

added theorem Nonneg.bot_eq

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

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/GroupTheory/Commutator/Basic.lean