Commit 2025-09-21 21:36 69e74d59

View on Github →

chore(RingTheory/AdicValuation): golf using WithZero.log (#27108) with helper lemma of how log preserves order

Estimated changes

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

added theorem WithZero.le_exp_log

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean