Commit 2025-08-27 10:43 b2c604b3

View on Github →

refactor: add assert_not_exists Field to Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (#28721)

  • Add assert_not_exists Field to Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
  • Split out semifields from Mathlib.Algebra.Order.Floor.Semiring into new file Mathlib.Algebra.Order.Floor.Semifield
  • Remove Field imports in Mathlib.Algebra.Order.Floor.Defs

Estimated changes

added theorem Nat.ceil_le_mul
added theorem Nat.ceil_le_two_mul
added theorem Nat.ceil_lt_mul
added theorem Nat.ceil_lt_two_mul
added theorem Nat.div_two_lt_floor
added theorem Nat.floor_div_eq_div
added theorem Nat.floor_div_natCast
added theorem Nat.floor_div_ofNat
added theorem Nat.mul_lt_floor
deleted theorem Nat.ceil_le_mul
deleted theorem Nat.ceil_le_two_mul
deleted theorem Nat.ceil_lt_mul
deleted theorem Nat.ceil_lt_two_mul
deleted theorem Nat.div_two_lt_floor
deleted theorem Nat.floor_div_eq_div
deleted theorem Nat.floor_div_natCast
deleted theorem Nat.floor_div_ofNat
deleted theorem Nat.mul_lt_floor