Commit 2025-09-29 07:22 3fb157f9

View on Github →

feat: one_sub_one_div_cast_* theorems (#28445)

Estimated changes

Modified Mathlib/Data/Nat/Cast/Order/Field.lean

added theorem Nat.one_sub_one_div_cast_le_one

added theorem Nat.one_sub_one_div_cast_nonneg