CeilDiv.ceilDiv_nonpos
theorem CeilDiv.ceilDiv_nonpos :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : CeilDiv α β] ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
This is a theorem about the "ceiling division" operation. For any types `α` and `β` that are ordered additive commutative monoids with a scalar multiplication that always returns zero when multiplied with zero, and for any instance of the `CeilDiv` structure on these types, if a value `a` of type `α` is less than or equal to zero, then performing the ceiling division of any value `b` of type `β` by `a` will always yield zero. However, users are advised not to use this theorem directly, but to use `ceilDiv_nonpos` instead.
More concisely: For any ordered additive commutative monoids `α` and `β` with a scalar multiplication that always returns zero when multiplied with zero, and for any `CeilDiv` instance, if `a` is of type `α` and nonpositive, then `a % b = 0` for all `b` of type `β`.
|
ceilDiv_le_iff_le_smul
theorem ceilDiv_le_iff_le_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : CeilDiv α β] {a : α} {b c : β}, 0 < a → (b ⌈/⌉ a ≤ c ↔ b ≤ a • c)
This theorem states that for any types `α` and `β` that are ordered additive commutative monoids, with `α` being a scalar multiplication zero class and `β` having a ceiling division operation, and given elements `a` of `α` and `b` and `c` of `β` such that `a` is positive, then `b` ceiling divided by `a` is less than or equal to `c` if and only if `b` is less than or equal to `a` times `c`. In mathematical notation, this is saying that if $0 < a$ then $b ⌈/⌉ a ≤ c$ if and only if $b ≤ a \cdot c$.
More concisely: For any ordered additive commutative monoids `α` and `β` with `α` a scalar multiplication zero class, `β` having a ceiling division operation, and `a` a positive element of `α`, the ceiling division `b ⌈/⌉ a` of `b` by `a` in `β` is less than or equal to `c` if and only if `b` is less than or equal to `a` multiplied by `c` in `β`.
|
FloorDiv.floorDiv_nonpos
theorem FloorDiv.floorDiv_nonpos :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : FloorDiv α β] ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
This theorem, `FloorDiv.floorDiv_nonpos`, states that for any types `α` and `β` that are ordered additive commutative monoids, and where `α` is a scalar multiple of zero for `β`, if a given element `a` of type `α` is less than or equal to zero, then the floor division of any element `b` of type `β` by `a` is equal to zero. However, this theorem is deprecated and it is recommended to use `floorDiv_nonpos` instead.
More concisely: For ordered additive commutative monoids `α` and `β` with `α` a scalar multiple of zero for `β`, if `a ∈ α` is nonpositive, then `b ÷ a = 0` for all `b ∈ β`.
|
floorDiv_of_nonpos
theorem floorDiv_of_nonpos :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : FloorDiv α β] {a : α}, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
This theorem, `floorDiv_of_nonpos`, states that for any types `α` and `β` where `α` is an ordered additive commutative monoid, `β` is also an ordered additive commutative monoid, `α` is a scaled multiplication zero class, and `α` has a floor division operation, if a value `a` of type `α` is less than or equal to zero, then the floor division of any value `b` of type `β` by `a` is always equal to zero.
More concisely: For ordered additive commutative monoids `α` and `β`, if `α` is a scaled multiplication zero class with floor division, and `a` is a value in `α` less than or equal to zero, then for all `b` in `β`, the floor division `b ⊥ a` equals zero.
|
CeilDiv.ceilDiv_gc
theorem CeilDiv.ceilDiv_gc :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : CeilDiv α β] ⦃a : α⦄,
0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
The theorem `CeilDiv.ceilDiv_gc` states that for any types `α` and `β` which are ordered additive commutative monoids, and for which `α` is a scalar multiplication zero class of `β`, and given an instance of `CeilDiv` for `α` and `β`, there is a Galois connection between the function that applies the ceiling division operation by some positive `a` of type `α` to `x` and another function that multiplies `a` by `x`. The theorem emphasizes not to use this directly, but rather to use `gc_smul_ceilDiv` or `gc_mul_ceilDiv` instead. Galois connection here means that for all `a : α` and `b : β`, `a ⌈/⌉ b ≤ x` if and only if `a ≤ a • x`, where `⌈/⌉` is the ceiling division operation and `•` denotes scalar multiplication.
More concisely: For types `α` and `β` being ordered additive commutative monoids with `α` as a scalar multiplication zero class of `β`, and given an instance of `CeilDiv` for `α` and `β`, there exists a Galois connection between the functions that apply ceiling division by some positive `α` element and scalar multiplication by that same element.
|
gc_floorDiv_smul
theorem gc_floorDiv_smul :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : FloorDiv α β] {a : α},
0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
The theorem `gc_floorDiv_smul` states that, for any types `α` and `β` which are ordered additive commutative monoids, and for any `a` in `α` which is greater than zero, the functions `a • x` and `x ⌊/⌋ a` form a Galois connection. This means that for all `x` in `α` and `y` in `β`, `a` times `x` is less than or equal to `y` if and only if `x` is less than or equal to the floor division of `y` by `a`. Here, `a • x` denotes the scaled version of `x` by a factor of `a`, and `x ⌊/⌋ a` denotes the floor division of `x` by `a`.
More concisely: For types `α` and `β` being ordered additive commutative monoids, and for any positive `a` in `α`, the functions `a • x` and `x ⌊/⌋ a` form a Galois connection, that is, `a • x ≤ y` if and only if `x ≤ y ∖ a` for all `x` in `α` and `y` in `β`.
|
FloorDiv.floorDiv_gc
theorem FloorDiv.floorDiv_gc :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : FloorDiv α β] ⦃a : α⦄,
0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
The theorem `FloorDiv.floorDiv_gc` states that for any types `α` and `β` that are ordered, additive, commutative monoids (i.e., they support well-behaved addition and zero operations), where `α` is also a "smul" zero class (meaning scalar multiplication with zero results in zero), and `α` supports floor division into `β`, if we have a positive value `a` of type `α`, then there exists a Galois connection between the function that scales by `a` and the function that floor divides by `a`. This Galois connection guarantees that for every pair of values in `α` and `β`, scaling the `α` value by `a` is less than or equal to the `β` value if and only if the `α` value is less than or equal to the `β` value floor divided by `a`.
More concisely: For ordered, additive commutative monoids `α` and `β` where `α` is a smul zero class and supports floor division into `β`, there exists a Galois connection between the function that scales `α` by a positive `α` value `a` and the function that floor divides `β` by `a`, such that `x ≤ y` in `α` if and only if `(x / a) ≤ y` in `β`.
|
gc_smul_ceilDiv
theorem gc_smul_ceilDiv :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : CeilDiv α β] {a : α},
0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
The theorem `gc_smul_ceilDiv` states that for any type `α` and `β` that have the structure of an ordered additive commutative monoid, with `α` also having a scalar multiplication by zero structure (`SMulZeroClass`) and `β` having a ceiling division structure (`CeilDiv`), and given any element `a` of type `α` which is greater than zero, a Galois connection exists between the function that maps `x` to the ceiling division of `x` by `a` and the function that maps `x` to the scalar multiple of `a` and `x`. This means that for all `x` and `y` of type `α` and `β` respectively, `x ⌈/⌉ a ≤ y` if and only if `x ≤ a • y`.
More concisely: For types `α` and `β` with ordered additive commutative monoid structures, where `α` has a scalar multiplication by zero and `β` has a ceiling division, and for any positive `a` in `α`, there exists a Galois connection between the function mapping `x` to `⌈x/a⌉` and the function mapping `x` to `a • x`. Therefore, `x ⌈/⌉ a ≤ y` if and only if `x ≤ a • y`.
|
zero_ceilDiv
theorem zero_ceilDiv :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : CeilDiv α β] (a : α), 0 ⌈/⌉ a = 0
The theorem `zero_ceilDiv` states that for all types `α` and `β`, given that these types have an ordered additive commutative monoid structure, can be scaled by zero, and have a 'ceiling division' operation, the ceiling division of zero by any instance `a` of type `α` always equals zero. In mathematical terms, for any `a` in an ordered additive commutative monoid, `0 ⌈/⌉ a = 0`. This signifies that dividing zero by any number and rounding up to the nearest integer is always zero.
More concisely: For any ordered additive commutative monoid type `α` with a ceiling division operation, `0 ⌈/⌉ a = 0` for all `a` in `α`.
|
FloorDiv.zero_floorDiv
theorem FloorDiv.zero_floorDiv :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : FloorDiv α β] (a : α), 0 ⌊/⌋ a = 0
This theorem, `FloorDiv.zero_floorDiv`, states that for any two types `α` and `β` with an ordered additive commutative monoid (which is a type of mathematical structure that involves ordered addition operation) and where `α` is a scaled multiplication zero class and there exists a floor division between `α` and `β`, the floor division of zero by any element of type `α` is always zero. This theorem is strongly discouraged to be used and the use of `zero_floorDiv` is recommended instead.
More concisely: For types `α` and `β` with an ordered additive commutative monoid structure, where `α` is a scaled multiplication zero class and there's a floor division between `α` and `β`, the floor division of zero by any `α` is equal to zero.
|
le_floorDiv_iff_smul_le
theorem le_floorDiv_iff_smul_le :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : FloorDiv α β] {a : α} {b c : β}, 0 < a → (c ≤ b ⌊/⌋ a ↔ a • c ≤ b)
This theorem asserts that for any types `α` and `β` with ordered additive commutative monoid structures, an action of `α` on `β` that respects zero, and a floor division operation from `α` to `β`, given non-zero elements `a` of `α` and `b` and `c` of `β`, the condition that `c` is less than or equal to the floor division of `b` by `a` is equivalent to the condition that the scalar multiplication of `a` and `c` is less than or equal to `b`.
More concisely: For types `α` and `β` with ordered additive commutative monoid structures, an action of `α` on `β` preserving zero, and a floor division operation from `α` to `β`, the floor division `b / a ≤ c` is equivalent to `a * c ≤ b`.
|
CeilDiv.zero_ceilDiv
theorem CeilDiv.zero_ceilDiv :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [self : CeilDiv α β] (a : α), 0 ⌈/⌉ a = 0
This theorem, `CeilDiv.zero_ceilDiv`, states that for any types `α` and `β` that are ordered additive commutative monoids, and any scalar multiplication of `α` and `β` where multiplication by zero yields zero, the ceiling division of zero by any element `a` of type `α` is zero. However, it is recommended not to use this theorem directly, and instead use `zero_ceilDiv`.
More concisely: For any ordered additive commutative monoids `α` and `β` with scalar multiplication where 0 multiplies any element to 0, the ceiling division of 0 by any `α` element is 0.
|
zero_floorDiv
theorem zero_floorDiv :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : FloorDiv α β] (a : α), 0 ⌊/⌋ a = 0
This theorem, `zero_floorDiv`, states that for any types `α` and `β` that together form an ordered additive commutative monoid, with `α` also being a scalar multiplication zero class, and an operation of floor division defined over `α` and `β`, the floor division of zero by any element `a` of type `α` equals zero. In other words, if we take any `a` in `α`, the floor division of 0 by `a` will always yield 0. This is analogous to the mathematical property that 0 divided by any number is always 0.
More concisely: For any ordered additive commutative monoid types `α` and `β` with `α` being a scalar multiplication zero class, if `α` has a floor division operation defined over `β`, then 0 ∥ 0 = 0, where ∥ denotes floor division.
|
ceilDiv_of_nonpos
theorem ceilDiv_of_nonpos :
∀ {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : OrderedAddCommMonoid β]
[inst_2 : SMulZeroClass α β] [inst_3 : CeilDiv α β] {a : α}, a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
The theorem `ceilDiv_of_nonpos` states that for any types `α` and `β`, given that they are ordered additive commutative monoids, and α is a scalar multiplication zero class, and there exists a ceiling division operation for α and β, if a value `a` of type `α` is less than or equal to 0, then the ceiling division of any value `b` of type `β` by `a` is equal to 0.
More concisely: For any ordered additive commutative monoids types `α` and `β` with `α` being a scalar multiplication zero class, if there exists a ceiling division operation for `α` and `β`, then for any `a` of type `α` less than or equal to 0 and any `b` of type `β`, their ceiling division `b / a` equals 0.
|