Commit 2024-07-09 11:47 e0e0819f

View on Github →

chore (Data.Nat.Cast.Field): split into unbundled and bundled results (#14536) We split off the results depending on LinearOrderedSemifield into a separate file.

Estimated changes

Modified Archive/OxfordInvariants/Summer2021/Week3P1.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Lemmas.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

Modified Mathlib/Data/ENat/Basic.lean

Modified Mathlib/Data/Int/Interval.lean

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

deleted theorem Nat.cast_div_le

deleted theorem Nat.cast_inv_le_one

deleted theorem Nat.inv_pos_of_nat

deleted theorem Nat.one_div_le_one_div

deleted theorem Nat.one_div_lt_one_div

deleted theorem Nat.one_div_pos_of_nat

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

added theorem Nat.cast_div_le

added theorem Nat.cast_inv_le_one

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