Commit 2024-01-08 14:36 aab088c2

View on Github →

feat: n⁻¹ ≤ 1 (#9533) From LeanAPAP

Estimated changes

added theorem Nat.cast_inv_le_one