Theorem Nat.one_sub_one_div_cast_le_one

Modification history

2026-10-31 01:50
Mathlib/Data/Nat/Cast/Order/Field.lean
chore(Data/Nat/Cast): remove redundant order instances (#45515) …
Modified Nat.one_sub_one_div_cast_le_oneView on Github →
2025-09-29 07:22
Mathlib/Data/Nat/Cast/Order/Field.lean
feat: `one_sub_one_div_cast_*` theorems (#28445)
Added Nat.one_sub_one_div_cast_le_oneView on Github →