Theorem NeZero.of_ge

Modification history

2025-06-09 09:08
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
feat(Data/Fin): `Fin.castLE` on the result of a cast from `Nat` (#25083)
Added NeZero.of_geView on Github →