Theorem WithZero.exists_exp_neg_natCast_lt

Modification history

2026-05-25 14:55
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
feat: elements of Dedekind domain approximate elements of valuation ring (#37523) …
Added WithZero.exists_exp_neg_natCast_ltView on Github →