Commit 2022-12-22 12:46 e35fccbf

View on Github →

feat: port Data.Nat.Cast.Field (#1161)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Cast/Field.lean

added theorem Nat.cast_div

added theorem Nat.cast_div_div_div_cancel_right

added theorem Nat.cast_div_le

added theorem Nat.inv_pos_of_nat

added theorem Nat.one_div_le_one_div

added theorem Nat.one_div_lt_one_div

added theorem Nat.one_div_pos_of_nat