Commit 2026-07-29 15:39 3edb3c06

feat(Algebra/GroupWithZero/WithZero): toAdd_unzero_eq_log and simplify proofs (#42149) This PR adds the lemma

lemma toAdd_unzero_eq_log {x : Mᵐ⁰} (hx : x ≠ 0) :
    (unzero hx).toAdd = log x

and uses it to simplify some proofs involving log, exp, and rank-one discrete valuations.