SetLike.coe_list_dProd
theorem SetLike.coe_list_dProd :
∀ {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : Monoid R]
[inst_2 : AddMonoid ι] (A : ι → S) [inst_3 : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a)))
(l : List α), ↑(l.dProd fι fA) = (List.map (fun a => ↑(fA a)) l).prod
The theorem `SetLike.coe_list_dProd` states that for any types ι, R, α, and S, given a SetLike relationship between S and R, a Monoid structure on R and an AddMonoid structure on ι, a function A mapping ι to S, a GradedMonoid structure on A, a function fι mapping α to ι and a function fA that maps a value of type α to a subtype of A at fι(a), and a list l of type α, the coercion of the dependent product of the subtypes (obtained with fι and fA on the list l) is equal to the product of the list obtained by applying the map function to the list l with a function that takes an element a and returns the coercion of fA at a. In simpler terms, it asserts that the process of taking the dependent product of subtypes and then coercing to the original type can be reordered with applying the coercion first and then taking the regular product.
More concisely: For any types ι, R, α, and S with a SetLike relationship, a Monoid structure on R, an AddMonoid structure on ι, a GradedMonoid structure on a function A from ι to S, a function fι mapping α to ι, a function fA, and a list l of type α, the coercion of the dependent product of subtypes obtained with fι and fA on l is equal to the product of the list obtained by applying the map function to l with the coercion of fA.
|
SetLike.GradedMul.mul_mem
theorem SetLike.GradedMul.mul_mem :
∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Mul R] [inst_2 : Add ι] {A : ι → S}
[self : SetLike.GradedMul A] ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)
The `SetLike.GradedMul.mul_mem` theorem is a statement about the homogeneity of multiplication. Specifically, it takes as input a set `A` indexed by a type `ι`, where `A` is a "set-like" object over a ring `R`. If `gi` is an element of `A` at index `i`, and `gj` is an element of `A` at index `j`, then their product `gi * gj` is an element of `A` at index `i + j`. This theorem holds under the conditions that `S` is a set-like view of `R` and that the operations of multiplication on `R` and addition on `ι` are defined. This can be interpreted as the property that multiplication distributes over the indexing in the set-like object `A`.
More concisely: If `A` is a set-like object over a ring `R` with index type `ι` and `gi` and `gj` are elements of `A` at indices `i` and `j` respectively, then `gi * gj` is an element of `A` at index `i + j`.
|
SetLike.mul_mem_graded
theorem SetLike.mul_mem_graded :
∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Mul R] [inst_2 : Add ι] {A : ι → S}
[inst_3 : SetLike.GradedMul A] ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)
This theorem states that for any types ι, R, and S, given that S is a set of R, R has a multiplication operation, and ι has an addition operation, and given a function A : ι → S that assigns each type ι instance to a set of R (where A supports a notion of graded multiplication), if gi is an element of A at index i and gj is an element of A at index j, then the product of gi and gj is an element of A at index (i + j). In simpler terms, it states that the product of two elements in a graded multiplication structure is also in the structure, at the index that is the sum of the original indices.
More concisely: For any types ι, R, and S with R having multiplication and ι addition, given a graded multiplication structure A : ι → S, the product of two elements in A lies in A at the index of their sum.
|
GradedMonoid.GMonoid.one_mul
theorem GradedMonoid.GMonoid.one_mul :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A),
1 * a = a
This theorem states that for any graded monoid, the operation of multiplying an element of the monoid by the identity element 'one' on the left side results in the same original element. In other words, for any type `ι`, any function `A` from `ι` to some type, any additive monoid structure on `ι`, and any `GradedMonoid.GMonoid` structure on `A`, any element `a` of the graded monoid satisfies the equation `1 * a = a`. This is the left identity property in the context of graded monoids.
More concisely: For any graded monoid `A` over a commutative additive monoid `ι`, the multiplication by the identity element `one` from `ι` is the identity function on `A`.
|
GradedMonoid.GMonoid.mul_one
theorem GradedMonoid.GMonoid.mul_one :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A),
a * 1 = a
This theorem asserts that, for any type `ι`, any type-valued function `A` from `ι`, any instance `inst` of an additive monoid on `ι`, and any instance `self` of a graded monoid on `A`, the multiplication of any element `a` of the graded monoid `A` with `one` results in `a` itself. In other words, the operation of multiplying by `one` on the right is an identity operation in the context of the graded monoid `A`. This is a formalization of the well-known principle in mathematics that multiplying any number by one does not change the number.
More concisely: For any graded monoid `A` and its identity element `one`, the multiplication of any element `a` in `A` with `one` results in `a` itself.
|
SetLike.list_dProd_eq
theorem SetLike.list_dProd_eq :
∀ {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : Monoid R]
[inst_2 : AddMonoid ι] (A : ι → S) [inst_3 : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a)))
(l : List α), l.dProd fι fA = ⟨(List.map (fun a => ↑(fA a)) l).prod, ⋯⟩
This theorem, named `SetLike.list_dProd_eq`, states that for any types `ι`, `R`, `α`, and `S`, where `S` behaves like a set of `R` and `R` has a monoid structure, and `ι` has an additive monoid structure. Given a function `A` that maps `ι` to `S`, where `A` behaves like a graded monoid, and functions `fι` and `fA` that map type `α` to `ι` and to the subtype of `A(fι a)` respectively. For any list of `α` denoted as `l`, the directed product of `l` with `fι` and `fA` is equal to the subtype formed by taking the product of the list obtained by mapping `fA` to each element of `l` and taking their underlying elements (`↑(fA a)`), where the second component of the subtype is suppressed (`⋯`).
More concisely: For any types `ι`, `R`, `α`, and `S` with `S` being a set-like type over `R` and `R` a monoid, `ι` an additive monoid, `A : ��ype ι → S` a graded monoid, and functions `fι : α → ι` and `fA : α → A (fι)`, the directed product of `l : list α` with `fι` and `fA` equals the subtype of the product of the list `map fA l` and their underlying elements, where the second component is suppressed.
|
SetLike.GradedOne.one_mem
theorem SetLike.GradedOne.one_mem :
∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : One R] [inst_2 : Zero ι] {A : ι → S}
[self : SetLike.GradedOne A], 1 ∈ A 0
This theorem states that for any types ι, R, S and any function A from ι to S, under the conditions that S is a set-like structure over R, R has a multiplicative identity (denoted as 1), ι has an additive identity (denoted as 0), and A is graded with respect to one (as defined by the `SetLike.GradedOne` class), the multiplicative identity of R (1) is an element of the set A(0).
More concisely: For any type ι, set-like structure S over R with 1 as its multiplicative identity, function A : ι -> S that is graded with respect to one, and types ι having an additive identity 0, the element 1 of R is in the set A(0).
|
List.dProd_monoid
theorem List.dProd_monoid :
∀ (ι : Type u_1) {R : Type u_2} {α : Type u_3} [inst : AddMonoid ι] [inst_1 : Monoid R] (l : List α) (fι : α → ι)
(fA : α → R), l.dProd fι fA = (List.map fA l).prod
The theorem `List.dProd_monoid` states that when all the indexed types are the same, the dependent product of a list is just the regular product of the list. Given any type `ι` along with types `R` and `α`, and assuming `ι` forms an addition monoid and `R` forms a monoid, for any list `l` of type `α` and any two functions `fι` and `fA` from `α` to `ι` and `R` respectively, the dependent product of `l` with respect to `fι` and `fA` is equal to the regular product of the list obtained by mapping `fA` to `l`. In other words, it shows the equivalence of dependent product with regular product when applying the function `fA` to each element of the list `l` and summing them up.
More concisely: Given a monoid `ι` and a monoid `R`, if `ι` is the index type for a list `l` of type `α`, then the dependent product of `l` with respect to functions from `α` to `ι` and `R` is equal to the regular product of the list obtained by applying a function from `α` to `R` to each element of `l`.
|
GradedMonoid.GMonoid.gnpow_succ'
theorem GradedMonoid.GMonoid.gnpow_succ' :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [self : GradedMonoid.GMonoid A] (n : ℕ)
(a : GradedMonoid A),
GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) =
⟨n • a.fst, GradedMonoid.GMonoid.gnpow n a.snd⟩ * a
The theorem `GradedMonoid.GMonoid.gnpow_succ'` states that for any type `ι`, any type function `A` from `ι` to another type, provided that `ι` has an `AddMonoid` instance and `A` has a `GradedMonoid.GMonoid` instance, for any natural number `n` and any element `a` of the graded monoid `A`, the graded monoid element with grade equal to the successor of `n` times `a.fst`, and element equal to the `n.succ`-th power of `a.snd` in the `GradedMonoid.GMonoid` structure, is equal to the product of the graded monoid element with grade `n` times `a.fst` and element the `n`-th power of `a.snd`, and `a`. This means that for graded monoids, raising to the power of the successor of a natural number behaves as you would expect, in terms of multiplication and the scalar multiplication on the grading.
More concisely: For any graded monoid `A` over type `ι` with an `AddMonoid` instance for `ι` and a `GradedMonoid.GMonoid` instance for `A`, the graded monoid element with grade `n.succ` and `n`-th power of `a` is equal to the `n.succ`-fold product of the graded monoid element with grade `n` and `a`.
|
GradedMonoid.GMonoid.gnpow_zero'
theorem GradedMonoid.GMonoid.gnpow_zero' :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A),
GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1
The theorem `GradedMonoid.GMonoid.gnpow_zero'` states that for any graded monoid `GradedMonoid A` with an underlying set `ι` and a function `A` mapping `ι` to some other type `u_2`, along with an additive monoid structure on `ι`, the zeroth power of any element `a` of the graded monoid is equal to the identity element `1`. This is similar to the familiar property in basic algebra where any number to the power of zero is one. The zeroth power is obtained by using the function `GradedMonoid.GMonoid.gnpow` on the second component of `a` (denoted by `a.snd`), and the result is packaged into the graded monoid using the function `GradedMonoid.mk` with `0 • a.fst` as the first component. The expression `0 • a.fst` represents the zero scalar multiple of the first component of `a` (denoted by `a.fst`).
More concisely: For any graded monoid `GradedMonoid A` with an additive monoid structure on the index set, the zeroth power of any element is the identity element. Equivalently, the function `GradedMonoid.GMonoid.gnpow_zero'` asserts that for all `a` in `GradedMonoid A`, `GradedMonoid.mk 0 (a.fst) = a`.
|
GradedMonoid.list_prod_map_eq_dProd
theorem GradedMonoid.list_prod_map_eq_dProd :
∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A]
(l : List α) (f : α → GradedMonoid A),
(List.map f l).prod =
GradedMonoid.mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)
The theorem `GradedMonoid.list_prod_map_eq_dProd` states that for any type `ι`, any type `α`, any function `A` from `ι` to another type, given an additive monoid structure on `ι` and a graded monoid structure on `A`, and for any list `l` of elements of type `α` and a function `f` from `α` to `GradedMonoid A`, the product of the list obtained by mapping `f` over `l` is equal to a `GradedMonoid` element. This element is constructed using the `dProdIndex` of `l` with respect to `f i`'s first component as the first component, and the `dProd` of `l` with respect to `f i`'s first component and `f i`'s second component as the second component.
In simpler terms, this theorem connects the operations of mapping a function over a list and then taking the product, with the operation of direct product over the list with respect to the function's components.
More concisely: For any additive monoid `ι`, graded monoid `A`, function `A ι → GradedMonoid A`, list `l : α^ι`, and function `f : α → A`, the direct product of `l` with respect to `f i.1` is equal to the product of the list obtained by mapping `f` to `l`.
|
GradedMonoid.GCommMonoid.mul_comm
theorem GradedMonoid.GCommMonoid.mul_comm :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddCommMonoid ι] [self : GradedMonoid.GCommMonoid A]
(a b : GradedMonoid A), a * b = b * a
This theorem states that multiplication is commutative in a graded monoid. Specifically, for any type `ι` and a type-dependent function `A`, given an additive commutative monoid structure on `ι` and a graded commutative monoid structure on `A`, the multiplication of any two elements `a` and `b` of the graded monoid `A` (constructed as a sigma type over `ι`) is commutative, meaning `a * b = b * a`.
More concisely: In a graded monoid over a type `ι` with additive commutativity on `ι` and graded commutativity on the type-dependent function `A`, multiplication is commutative, i.e., `a * b = b * a` for all `a, b` in `A`.
|
GradedMonoid.mk_zero_smul
theorem GradedMonoid.mk_zero_smul :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddZeroClass ι] [inst_1 : GradedMonoid.GMul A] {i : ι} (a : A 0)
(b : A i), GradedMonoid.mk i (a • b) = GradedMonoid.mk 0 a * GradedMonoid.mk i b
The theorem `GradedMonoid.mk_zero_smul` states that for any type `ι`, any family of types `A : ι → Type`, given an additive zero class on `ι` and a graded multiplication on `A`, for any element `a` of type `A 0` and any element `b` of type `A i`, the element of the graded monoid constructed from `i` and the scalar product of `a` and `b` is equal to the multiplication of the elements of the graded monoid constructed from `0` and `a`, and `i` and `b`. In other words, it says that the scalar product can be moved out of the graded monoid construction.
More concisely: For any graded monoid `{A: ι → Type, ∏: ι × ι → A, 0: A 0, add: A → A → A, smul: ℝ → A 0 → A}`, where `ℝ` is the real numbers, the scalar multiplication of the graded monoid element `smul r a` by an element `a` in `A 0` and another element `b` in `A i` is equal to the graded monoid multiplication of the elements `smul r 0` and `a` with `b`.
|
GradedMonoid.GMonoid.mul_assoc
theorem GradedMonoid.GMonoid.mul_assoc :
∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [self : GradedMonoid.GMonoid A] (a b c : GradedMonoid A),
a * b * c = a * (b * c)
The theorem `GradedMonoid.GMonoid.mul_assoc` states that multiplication is associative in a graded monoid. Specifically, for any type `ι`, any type-valued function `A` (that assigns types to elements of `ι`), any `AddMonoid` instance for `ι`, and any `GradedMonoid` instance for `A`, the product of any three elements `a`, `b`, and `c` of the graded monoid `A` satisfies the property `a * b * c = a * (b * c)`. This means that the order in which the multiplication operations are performed does not affect the final result.
More concisely: In a graded monoid, the associativity of multiplication holds: `a * b * c = a * (b * c)` for all `a`, `b`, and `c` in the monoid.
|
SetLike.one_mem_graded
theorem SetLike.one_mem_graded :
∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : One R] [inst_2 : Zero ι] (A : ι → S)
[inst_3 : SetLike.GradedOne A], 1 ∈ A 0
This theorem, `SetLike.one_mem_graded`, asserts that for any types `ι`, `R` and `S`, with `S` being a set-like object over `R`, `R` being a type with a defined multiplicative identity (One), and `ι` being a type with a defined additive identity (Zero), if you have a graded function `A` from `ι` to `S`, such that `A` respects the multiplicative identity, then the multiplicative identity of `R` is an element of the set `A` of `0` (the additive identity of `ι`). In other words, in this graded structure, the multiplicative identity exists at the level of the additive identity.
More concisely: If `A` is a graded function from a type `ι` with additive identity `0` to a set-like object `S` over a type `R` with multiplicative identity `One`, such that `A` respects the multiplicative identity, then `One` is an element of `A(0)`.
|