Pi.mulSingle_commute
theorem Pi.mulSingle_commute :
∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)],
Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (Pi.mulSingle i x) (Pi.mulSingle j y)
The theorem `Pi.mulSingle_commute` states that for any type `I` and function `f` from `I` to a type, given that `I` has decidable equality and each `I` in `f` has a multiplication and a unit structure (`MulOneClass`), then for every pair of distinct indices `i` and `j`, the function `Pi.mulSingle` commutes for any elements `x` of `f i` and `y` of `f j`. In other words, the result of applying `Pi.mulSingle` to `x` and then to `y` is the same as applying `Pi.mulSingle` to `y` and then to `x`. Here, `Pi.mulSingle` is a function that takes an element `x` of `f i` and produces a function that returns `x` when given `i` and `1` otherwise. The `Commute` predicate states that two elements commute if their multiplication results in the same value regardless of the order in which they're multiplied.
More concisely: For any type `I` with decidable equality and functions `f : I → type with decidable eq and MulOneClass, the function `Pi.mulSingle` commutes, i.e., `Pi.mulSingle x ∘ Pi.mulSingle y = Pi.mulSingle y ∘ Pi.mulSingle x` for all distinct `i, j : I` and `x : f i`, `y : f j`.
|
Pi.mulSingle_apply_commute
theorem Pi.mulSingle_apply_commute :
∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)] (x : (i : I) → f i)
(i j : I), Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))
This theorem states that for any type `I` and a type-valued function `f` from `I`, given `I` and `f` have decidable equality and every `f i` for `i` in `I` is an instance of `MulOneClass`, then for any function `x` from `I` to `f i` and any two elements `i` and `j` in `I`, the functions `Pi.mulSingle i (x i)` and `Pi.mulSingle j (x j)` commute.
In simpler terms, this theorem is about functions that map each element of a type `I` to an element of a type `f i` (which is a type with multiplication and a multiplicative identity). It says that if you pick two elements from `I` and create two functions that are `1` everywhere except at those points (where they are the corresponding value of the function `x`), those two functions will commute, i.e., their multiplication is commutative.
More concisely: Given a type `I` and a type-valued function `f` from `I` where every `f i` is in the Multiplicative Monoid `MulOneClass`, if `x` is a function from `I` to `f i` and `i` and `j` are in `I`, then `Pi.mulSingle i (x i) * Pi.mulSingle j (x j) = Pi.mulSingle j (x j) * Pi.mulSingle i (x i)`.
|
Pi.single_apply_addCommute
theorem Pi.single_apply_addCommute :
∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (x : (i : I) → f i)
(i j : I), AddCommute (Pi.single i (x i)) (Pi.single j (x j))
This theorem states that for any given type `I`, a function `f` from `I` to another type `v`, along with instances of `DecidableEq` for `I` and `AddZeroClass` for `f i`, and any function `x` from `I` to `f i`, the function `Pi.single` (which supports a function at `i` with value `x(i)` and `0` elsewhere) possesses the additive commutative property. Specifically, for any two elements `i` and `j` in `I`, the sum of `Pi.single i (x i)` and `Pi.single j (x j)` is the same as the sum of `Pi.single j (x j)` and `Pi.single i (x i)`. In other words, we can swap the order of addition without changing the result.
More concisely: For any type `I`, function `f` from `I` to another type with DecidableEq and AddZeroClass instances, and function `x` from `I` to `f`, the functions `Pi.single i x(i)` and `Pi.single j x(j)` (i, j ∈ I) satisfy the additive commutative property: `Pi.single i x(i) + Pi.single j x(j) = Pi.single j x(j) + Pi.single i x(i)`.
|
Pi.single_addCommute
theorem Pi.single_addCommute :
∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)],
Pairwise fun i j => ∀ (x : f i) (y : f j), AddCommute (Pi.single i x) (Pi.single j y)
This theorem states that the operation of injecting into an additive pi group at different indices commutes. Given any type `I` and a type-valued function `f` over `I`, under the conditions that `I` has decidable equality and every type `f i` for `i : I` has an additive zero class, for any distinct indices `i` and `j` in `I` and for any elements `x` in `f i` and `y` in `f j`, the two elements injected into an additive pi group at these different indices commute. In other words, if `x` and `y` are injected into a pi group at different indices, the order of their addition doesn't matter. Note that this theorem considers the case of different indices; for the case of the same index, refer to `AddCommute.map`.
More concisely: Given a type `I` with decidable equality and a type-valued function `f` over `I` such that every `f i` has an additive zero, for distinct indices `i` and `j` in `I`, the commutativity of adding the elements `x : f i` and `y : f j` in an additive pi group, i.e., `x + (∑ i : I, f i) y = ∑ i : I, f i (x + y)`.
|