Commit 2024-01-09 17:16 25bcbbb6

View on Github →

feat: Flooring/ceiling division (#9149) This PR defines flooring and ceiling division as the right and left adjoints to the map b ↦ a • b.

Estimated changes

added theorem Finsupp.ceilDiv_apply
added theorem Finsupp.ceilDiv_def
added theorem Finsupp.floorDiv_apply
added theorem Finsupp.floorDiv_def
added theorem Nat.floorDiv_eq_div
added theorem Pi.ceilDiv_apply
added theorem Pi.ceilDiv_def
added theorem Pi.floorDiv_apply
added theorem Pi.floorDiv_def
added theorem ceilDiv_le_iff_le_mul
added theorem ceilDiv_le_iff_le_smul
added theorem ceilDiv_of_nonpos
added theorem ceilDiv_one
added theorem ceilDiv_zero
added theorem floorDiv_le_ceilDiv
added theorem floorDiv_of_nonpos
added theorem floorDiv_one
added theorem floorDiv_zero
added theorem gc_floorDiv_mul
added theorem gc_floorDiv_smul
added theorem gc_mul_ceilDiv
added theorem gc_smul_ceilDiv
added theorem le_floorDiv_iff_mul_le
added theorem le_smul_ceilDiv
added theorem smul_ceilDiv
added theorem smul_floorDiv
added theorem smul_floorDiv_le
added theorem zero_ceilDiv
added theorem zero_floorDiv