Theorem WithZero.exp_eq_coe_ofAdd

Modification history

2026-04-14 10:54
Mathlib/Algebra/GroupWithZero/WithZero.lean
feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …
Added WithZero.exp_eq_coe_ofAddView on Github →