Theorem WithZero.le_exp_log

Modification history

2025-09-21 21:36
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
chore(RingTheory/AdicValuation): golf using WithZero.log (#27108) …
Added WithZero.le_exp_logView on Github →