VAddMemClass.vadd_mem
theorem VAddMemClass.vadd_mem :
∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : VAdd R M] [inst_1 : SetLike S M]
[self : VAddMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ m ∈ s
This theorem states that for any set `S` of type `M`, any element `m` of `M` that belongs to `S`, and any scalar `r` of type `R`, if `M` has a vector addition operation (`VAdd`) defined, and `S` is a "set-like" structure for `M` (meaning you can add elements to `S` and check if an element is in `S`), then adding `r` and `m` via the vector addition operation results in an element that still belongs to `S`. Essentially, scalar addition with an element of the set results in an element that also belongs to the set.
More concisely: For any set `S` of type `M` with vector addition `VAdd`, and for any `m` in `S` and scalar `r`, the result `VAdd r m` is also in `S`.
|
SubMulAction.stabilizer_of_subMul
theorem SubMulAction.stabilizer_of_subMul :
∀ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
MulAction.stabilizer R m = MulAction.stabilizer R ↑m
This theorem states that for any group `R`, `M` with a multiplication action `R` on `M`, and any submultiplicative action `p` of `R` on `M`, and for any element `m` of the submultiplicative action `p`, the stabilizer of `m` in the group under the submultiplicative action is the same as the stabilizer of the corresponding element in the ambient space `M`. In other words, the subgroup of `R` that leaves `m` fixed under the action on `p` coincides with the subgroup of `R` that leaves the same element `m` in `M` fixed under the total action on `M`.
More concisely: For any group action `R` on `M` and submultiplicative action `p` of `R` on `M`, the stabilizer of an element `m` under `p` equals the stabilizer of `m` under the total action of `R` on `M`.
|
SMulMemClass.smul_mem
theorem SMulMemClass.smul_mem :
∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : SMul R M] [inst_1 : SetLike S M]
[self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s
The theorem `SMulMemClass.smul_mem` states that for any types `S`, `R`, and `M`, where `M` is a type with scalar multiplication by `R` (indicated by `[inst : SMul R M]`), and `S` is a set-like structure of `M` (indicated by `[inst_1 : SetLike S M]`), if we have an element `m` of `M` that belongs to `S` (expressed as `m ∈ s`), then the result of scalar multiplication of `m` by any scalar `r` from `R` (expressed as `r • m`) also belongs to `S`. This theorem ensures that scalar multiplication of an element in a set (or set-like structure) results in another element within the same set.
More concisely: For any set-like structure `S` over type `M` with scalar multiplication by `R`, if `m` is an element of `S` and `r` is any scalar in `R`, then `r • m` is also an element of `S`.
|
SubMulAction.smul_of_tower_mem
theorem SubMulAction.smul_of_tower_mem :
∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
[inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M}, x ∈ p → s • x ∈ p
This theorem states that for any types `S`, `R`, and `M`, where `R` is a monoid and `M` is a mulaction of `R`, and `S` interacts with `R` and `M` through scalar multiplication. If `S`, `R` and `M` form a scalar tower, and `p` is a submulaction of `R` on `M`, then for any element `s` of `S` and any element `x` of `M` that belongs to `p`, the result of scalar multiplication of `s` and `x` is also in `p`. This is essentially saying that the scalar multiplication operation is closed in the submulaction `p`.
More concisely: For any monoid `R` with mulaction `M`, scalar tower `S`, and submulaction `p` of `R` on `M`, if `s ∈ S` and `x ∈ p`, then `s * x ∈ p`, where `*` denotes scalar multiplication.
|
SubMulAction.stabilizer_of_subMul.submonoid
theorem SubMulAction.stabilizer_of_subMul.submonoid :
∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m
This theorem states that for any submultiplicative action `p` of a monoid `R` on a set `M`, and any element `m` in `p`, the stabilizer submonoid of `m` within the submultiplicative action is the same as the stabilizer submonoid of `m` in the larger context of the entire set `M`. In other words, the set of elements of `R` that fix `m` when acting on `M` is the same whether we consider `m` as an element of the subaction `p` or as an element of the whole space `M`. Here, "fixing" `m` means that, when the element of `R` acts on `m`, the result is `m` itself.
More concisely: For any submultiplicative action of a monoid on a set and any element in the set, the stabilizer submonoids of that element in the action and in the entire set are equal.
|
SubMulAction.val_image_orbit
theorem SubMulAction.val_image_orbit :
∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
Subtype.val '' MulAction.orbit R m = MulAction.orbit R ↑m
This theorem, named `SubMulAction.val_image_orbit`, states that for any types `R` and `M` where `R` has a monoid structure and `M` has `R` acting on it (a `MulAction`), and for any `SubMulAction` `p` of `R` on `M` and any element `m` of `p`, the image of the orbit of `m` under the `Subtype.val` function is equal to the orbit of the underlying element of `m` in the ambient space. In other words, the orbits in a `SubMulAction` coincide with the orbits in the ambient space.
More concisely: For any `R`-module `M` with an `R`-action `p` as a `SubMulAction` and any `m` in `p`, the image of `p.orbit m` under the `Subtype.val` function equals the orbit of `m` in `M`.
|
AddSubgroupClass.zsmulMemClass
theorem AddSubgroupClass.zsmulMemClass :
∀ {S : Type u_1} {M : Type u_2} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [inst_2 : AddSubgroupClass S M],
SMulMemClass S ℤ M
This theorem, `AddSubgroupClass.zsmulMemClass`, states that for any types `S` and `M`, given that `M` forms a subtractive, negatable monoid (`SubNegMonoid`), `S` behaves like a set of `M` (`SetLike S M`), and `S` is a class of additive subgroups of `M` (`AddSubgroupClass S M`), then `S` is a class that respects scalar multiplication with integers (`ℤ`) on `M` (`SMulMemClass S ℤ M`). In other words, it guarantees that, under these conditions, scalar multiplication with integers of elements in `S` will result in another element in `S`.
More concisely: Given a subtractive, negatable monoid `M` with set `S` of its additive subgroups that respects scalars multiplication by integers, then `S` is a set of `M` that respects scalar multiplication by integers.
|
AddSubmonoidClass.nsmulMemClass
theorem AddSubmonoidClass.nsmulMemClass :
∀ {S : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M],
SMulMemClass S ℕ M
This theorem is stating that for any types `S` and `M`, given that `M` is an additive monoid, `S` is a subset of `M`, and `S` is an additive submonoid of `M`, we can confirm that `S` belongs to the `SMulMemClass` with respect to `S`, natural numbers `ℕ`, and `M`. In simpler terms, the elements of `S` can be scalar multiplied by natural numbers to yield another element in `M`. This theorem is not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`.
More concisely: For any additive monoid `M` and subset `S` of `M` that is also an additive submonoid, `S` is a scalar multiplication submonoid of `M` by natural numbers.
|
SubMulAction.smul_mem
theorem SubMulAction.smul_mem :
∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x ∈ p → r • x ∈ p
This theorem states that for any scalar `r` of type `R` and any element `x` of type `M`, if `x` is an element of the SubMultiplicative Action `p`, then the result of scalar multiplication of `r` and `x` (notated as `r • x`) also belongs to `p`. In other words, if a scalar multiple of `x` is formed, it remains within the submultiplicative action `p`. Here, `R` and `M` are any types that support a scalar multiplication (`SMul R M`).
More concisely: For any scalar `r` in `R` and any element `x` in the submultiplicative action `p` over `M`, the scalar multiplication `r • x` belongs to `p`.
|
SMulMemClass.ofIsScalarTower
theorem SMulMemClass.ofIsScalarTower :
∀ (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [inst : SetLike S α] [inst_1 : SMul M N]
[inst_2 : SMul M α] [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α]
[inst_6 : IsScalarTower M N α], SMulMemClass S M α
This theorem, `SMulMemClass.ofIsScalarTower`, asserts that for any types `S`, `M`, `N`, and `α` such that `S` behaves like a set of `α`s (`SetLike S α`), `M` and `N` are scalar multipliers of `α` (`SMul M α` and `SMul N α`), `N` has a monoid structure (`Monoid N`), `N` acts on `α` (`MulAction N α`), the scalar multiplication of elements from `S` and `N` always results in an element in `α` (`SMulMemClass S N α`), and `M`, `N`, and `α` form a scalar tower (`IsScalarTower M N α`), then `S` and `M` scalar multiplication also always results in an element in `α` (`SMulMemClass S M α`). In simpler terms, if scalar multiplication by `N` keeps us in `α`, and `M`, `N`, and `α` form a scalar tower, then scalar multiplication by `M` also keeps us in `α`.
More concisely: If `S` is a set-like collection of scalars for type `α`, `M` and `N` are scalar multipliers for `α` with `N` being a monoid, `N` acts on `α`, `SMul MemClass` holds for `S`, `N`, and `α`, and `M`, `N`, and `α` form a scalar tower, then `SMul MemClass` also holds for `S` and `M` with respect to `α`.
|
SubMulAction.smul_mem'
theorem SubMulAction.smul_mem' :
∀ {R : Type u} {M : Type v} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
x ∈ self.carrier → c • x ∈ self.carrier
This theorem states that, for any scalar `c` and any element `x` of a given subset of a scalar multiplication operation (`SMul`), if `x` is part of the `carrier` (the given subset), then the result of scalar multiplication of `c` and `x` (denoted as `c • x`) is also part of the `carrier`. In other words, the `carrier` set is closed under scalar multiplication in the context of a scalar multiplication action (`SubMulAction`).
More concisely: For any subset `S` of a scalar multiplication operation `SMul` and any scalar `c` and element `x` in `S`, the result `c • x` is also in `S`. In other words, the scalar multiplication operation `SMul` preserves the subset `S`.
|