Commit 2026-05-19 19:46 50e18555

View on Github →

chore: deprecate WithZero.zero_le (#39016) This is a duplicate of zero_le in the root namespace.

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

deleted theorem WithZero.zero_le

Modified Mathlib/FieldTheory/RatFunc/Valuation.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean