Theorem Nat.cast_inv_le_one

Modification history

2024-07-09 11:47
Mathlib/Data/Nat/Cast/Field.lean
chore (Data.Nat.Cast.Field): split into unbundled and bundled results (#14536) …
Modified Nat.cast_inv_le_oneView on Github →
2024-01-08 14:36
Mathlib/Data/Nat/Cast/Field.lean
feat: `n⁻¹ ≤ 1` (#9533) …
Added Nat.cast_inv_le_oneView on Github →