Theorem WithZero.toAdd_unzero_eq_log

Modification history

2026-07-29 15:39

Mathlib/Algebra/GroupWithZero/WithZero.lean

feat(Algebra/GroupWithZero/WithZero): `toAdd_unzero_eq_log` and simplify proofs (#42149) …

Added WithZero.toAdd_unzero_eq_log View on Github →