Revision #3481 → #4030 · back to history
modifiedFloor function0896cfc66dd2
| Field | From #3481 | To #4030 |
|---|
| note | `Int.floor a` is defined as the greatest integer z with z ≤ a via the FloorRing class. | `Int.floor a` is the greatest integer z with z ≤ a via the FloorRing class. |
modifiedCeiling function299780286850
| Field | From #3481 | To #4030 |
|---|
| note | `Int.ceil a` is defined as the smallest integer z with a ≤ z via the FloorRing class. | `Int.ceil a` is the smallest integer z with a ≤ z via the FloorRing class. |
modifiedfloor(x+1) vs ceil(x) at integersc6d5e81e8594
| Field | From #3481 | To #4030 |
|---|
| note | Mathlib has `ceil_eq_floor_add_one_iff_notMem` characterizing exactly the case where ⌈x⌉ = ⌊x⌋+1, i.e. x is not an integer. | `ceil_eq_floor_add_one_iff_notMem` characterises exactly the case where ⌈x⌉ = ⌊x⌋+1, i.e. x is not an integer. |
modifiedFloor and ceiling via defining equations5d0ac7ab5dcc
| Field | From #3481 | To #4030 |
|---|
| note | `Int.floor_eq_iff` and `Int.ceil_eq_iff` characterize the floor/ceiling exactly by the defining inequalities. | `Int.floor_eq_iff` and `Int.ceil_eq_iff` characterise the floor/ceiling by the defining inequalities. |
modifiedFloor as residuated mapping / Galois connection20d7fb834273
| Field | From #3481 | To #4030 |
|---|
| note | `Int.gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor` records the Galois (residuated) connection. | `Int.gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor` records the residuated/Galois connection. |
modifiedFloor ≤ ceiling, equality iff integer3d9da6b492d7
| Field | From #3481 | To #4030 |
|---|
| note | `Int.floor_le_ceil` gives ⌊a⌋ ≤ ⌈a⌉, and `floor_eq_self_iff_mem`/`ceil_eq_self_iff_mem` characterize equality with integers. | `Int.floor_le_ceil` gives ⌊a⌋ ≤ ⌈a⌉, and `floor_eq_self_iff_mem`/`ceil_eq_self_iff_mem` characterise equality with integers. |
modifiedIdempotence of floor, ceiling, fractional parta8beb369bc9c
| Field | From #3481 | To #4030 |
|---|
| note | `Int.fract_fract` shows fract idempotent; `floor_intCast`/`ceil_intCast` give idempotence on integer outputs. | `Int.fract_fract` shows fract is idempotent; `floor_intCast`/`ceil_intCast` give idempotence for integer outputs. |
modifiedInteger quotient floor identity9c9813a6aaa8
| Field | From #3481 | To #4030 |
|---|
| note | `Rat.floor_intCast_div_natCast` and `Int.floor_div_natCast` cover floor of integer-division-style quotients for nonneg denominators. | `Rat.floor_intCast_div_natCast` and `Int.floor_div_natCast` cover floor of integer-division-style quotients for non-negative denominators. |
modifiedNested divisions identity9fc07edabb0a
| Field | From #3481 | To #4030 |
|---|
| note | `Nat.floor_div_eq_div` and `Int.floor_div_natCast` handle the integer case; nested-division identities like ⌊⌊x/m⌋/n⌋ = ⌊x/(mn)⌋ are not stated explicitly. | `Nat.floor_div_eq_div` and `Int.floor_div_natCast` handle the integer case; the ⌊⌊x/m⌋/n⌋ = ⌊x/(mn)⌋ identity is not stated explicitly. |
modifiedQuadratic reciprocity via floor4154851b0bb1
| Field | From #3481 | To #4030 |
|---|
| note | `ZMod.quadratic_reciprocity` (and `ZMod.eisenstein_lemma`) formalize quadratic reciprocity via the Eisenstein floor-sum method. | `legendreSym.quadratic_reciprocity` (and `ZMod.eisenstein_lemma`) formalize quadratic reciprocity via the Eisenstein floor-sum method. |
modifiedRounding to nearest integer (ties up)034d4702527e
| Field | From #3481 | To #4030 |
|---|
| note | `round x := ⌊x + 1/2⌋`-style definition in `Mathlib.Algebra.Order.Round` rounds ties towards +∞. | `round` in `Mathlib.Algebra.Order.Round` performs round-half-up (⌊x + 1/2⌋-style). |
modifiedBeatty sequence partition57f19aff5d57
| Field | From #3481 | To #4030 |
|---|
| note | `Irrational.beattySeq_symmDiff_beattySeq_pos` formalizes Rayleigh/Beatty's theorem on partitioning positive integers. | `Irrational.beattySeq_symmDiff_beattySeq_pos` formalises Rayleigh/Beatty's theorem on partitioning positive integers. |
modifiedPrime counting via Wilson's theorem25ca8fe9dc1c
| Field | From #3481 | To #4030 |
|---|
| note | Wilson's theorem is formalized as `Nat.prime_iff_fac_equiv_neg_one`, but its floor-based prime-counting consequence is not. | Wilson's theorem is formalised as `Nat.prime_iff_fac_equiv_neg_one`, but its floor-based prime-counting consequence is not. |
modifiedRamanujan's floor function problems6bff973ea0a2
| Field | From #3481 | To #4030 |
|---|
| note | Ramanujan's floor identities are not formalized. | Ramanujan's floor identities are not formalised. |
modifiedFloor floor identity (nested floor)074f914104fe
| Field | From #3481 | To #4030 |
|---|
| note | Additional coverage: `Nat.floor_div_natCast` gives ⌊x / n⌋₊ = ⌊x⌋₊ / n for x : α and n : ℕ, a special case of the nested-division identity (corrected from nonexistent `Nat.floor_div_nat`). | `Nat.floor_div_natCast` gives ⌊x / n⌋₊ = ⌊x⌋₊ / n for x : α and n : ℕ, a special case of the nested-division identity. |