Theorem Nat.one_div_cast_ne_zero

Modification history

2024-10-28 10:31
Mathlib/Data/Nat/Cast/Order/Field.lean
feat(Algebra/Order/Field/Basic): add Nat cast lemmas (#18171) …
Added Nat.one_div_cast_ne_zeroView on Github →