QuotientAddGroup.out_eq'
theorem QuotientAddGroup.out_eq' :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (a : α ⧸ s), ↑(Quotient.out' a) = a
The theorem `QuotientAddGroup.out_eq'` states that for any type `α` equipped with an additive group structure, given an additive subgroup `s` of `α` and an element `a` of the quotient group `α ⧸ s`, the canonical projection of the outcome of the function `Quotient.out'` applied to `a` is equal to `a`. In other words, it says that applying the function `Quotient.out'`, which retrieves a representative element from the equivalence class in the quotient group, and then mapping back to the quotient group via the canonical projection, gives us the original element `a` of the quotient group. This theorem essentially validates the correctness of the function `Quotient.out'` in the context of additive quotient groups.
More concisely: For any additive group `α` and its subgroup `s`, the canonical projection of the representative element of an equivalence class `a` in the quotient group `α ⧸ s` is equal to `a` itself.
|
QuotientAddGroup.induction_on
theorem QuotientAddGroup.induction_on :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
This theorem, `QuotientAddGroup.induction_on`, defines an induction principle for elements of the quotient group of an additive group `α` by an additive subgroup `s`. Given a property `C` that applies to elements of the quotient group `α ⧸ s`, if every element `z` of the original group `α` satisfies the property `C` when considered in the quotient group (i.e., `C ↑z`), then every element `x` of the quotient group also satisfies `C`. This allows us to reason about all elements of the quotient group by only considering elements of the original group.
More concisely: If a property holds for every coset representative of an additive subgroup of an abelian group, then it holds for all elements in the quotient group.
|
Subgroup.card_eq_card_quotient_mul_card_subgroup
theorem Subgroup.card_eq_card_quotient_mul_card_subgroup :
∀ {α : Type u_1} [inst : Group α] [inst_1 : Fintype α] (s : Subgroup α) [inst_2 : Fintype ↥s]
[inst_3 : DecidablePred fun a => a ∈ s], Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card ↥s
The theorem `Subgroup.card_eq_card_quotient_mul_card_subgroup` states that for any given type `α` that has a group structure and is finite (`Fintype`), and a subgroup `s` of `α` that is also finite, the cardinality (i.e., the number of elements) of `α` is equal to the product of the cardinality of the quotient group `α ⧸ s` and the cardinality of the subgroup `s` itself. This is under the condition that the predicate "a is an element of `s`" is decidable for all `a` in `α`, i.e., for any element of the group, we can determine whether or not it belongs to the subgroup `s`. This theorem is a version of the Lagrange's theorem in group theory, which states that the order of any finite group is the product of the order of a subgroup and the order of the quotient group formed by dividing the group by that subgroup.
More concisely: For any finite group `α` with a decidable subgroup `s`, the cardinality of `α` equals the product of the cardinalities of `α/s` and `s`.
|
Mathlib.GroupTheory.Coset._auxAddLemma.2
theorem Mathlib.GroupTheory.Coset._auxAddLemma.2 :
∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), (x ∈ a +ᵥ s) = (-a + x ∈ s)
This theorem states that for any type `α` with an addition group structure, for any set `s` of elements of type `α`, and for any elements `x` and `a` of type `α`, the statement that `x` belongs to the coset formed by adding `a` to every element in `s` (denoted as `a +ᵥ s`) is logically equivalent to the statement that the result of adding the additive inverse of `a` to `x` belongs to the set `s` (denoted as `-a + x ∈ s`).
In simple mathematical terms, it states that if `x` is in the set formed by adding `a` to every element in `s`, then subtracting `a` from `x` will result in an element that is in the original set `s`.
More concisely: For any type `α` with an addition group structure, and for any set `s` and element `a` of type `α`, the coset `a +ᵥ s` is equal to the set `{x | -a + x ∈ s}` (i.e., the set of elements obtained by adding `a` to every element in `s` is equal to the set of elements in `s` whose additive inverse is also in `s`).
|
QuotientAddGroup.rightRel_apply
theorem QuotientAddGroup.rightRel_apply :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ y + -x ∈ s
This theorem, `QuotientAddGroup.rightRel_apply`, states that for any type 'α' which is an additive group, and for any additive subgroup 's' of 'α', and for any elements 'x' and 'y' of 'α', the equivalence relation (denoted as `Setoid.r`) for 'x' and 'y' holds if and only if the result of adding the additive inverse of 'x' to 'y' belongs to the subgroup 's'. In other words, 'x' and 'y' are in the same equivalence class under the given setoid iff 'y - x' is an element of the subgroup 's'.
More concisely: For any additive group 'α' and additive subgroup 's' of 'α', 'x' and 'y' are in the same equivalence class of the subgroup 's' if and only if 'y - x' is an element of 's'.
|
one_leftCoset
theorem one_leftCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), 1 • s = s
This theorem, `one_leftCoset`, states that for all types `α` endowed with a `Monoid` structure, for any set `s` of elements of type `α`, the left coset of `s` by `1` (denoted as `1 • s`) is equal to `s` itself. In mathematical terms, when we "act" on the set `s` by the multiplicative identity of the monoid (which is `1`), the set remains unchanged. This result is a fundamental property in group theory, specifically in the study of cosets.
More concisely: For any set `s` of elements in a monoid `α`, the left coset `1 • s` equals `s`.
|
QuotientGroup.induction_on
theorem QuotientGroup.induction_on :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x := by
sorry
This theorem, named `QuotientGroup.induction_on`, is an induction principle for quotient groups. It states for a given type `α`, which has a group structure, subgroup `s`, and a proposition `C` about the elements of the quotient group `α ⧸ s`, if `C` holds for all elements of `α` when viewed as elements of `α ⧸ s`, then `C` holds for every element of `α ⧸ s`. Essentially, it allows us to prove something about all elements of a quotient group by proving it for all elements of the original group.
More concisely: Given a group `α` with a subgroup `s`, if `C` holds for all `α` elements in their quotient group `α / s`, then `C` holds for every element of `α / s`.
|
mem_leftAddCoset_iff
theorem mem_leftAddCoset_iff :
∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ a +ᵥ s ↔ -a + x ∈ s
This theorem states that for all types `α` which form an additive group, given a set `s` of elements of type `α`, an element `x` of type `α`, and another element `a` of type `α`, `x` belongs to the coset formed by adding `a` to every element of `s` if and only if the element obtained by adding the additive inverse of `a` to `x` belongs to `s`. In mathematical terms, this theorem can be represented as follows: For any additive group `α` and any subset `s` in `α`, $x \in a + s$ if and only if $-a + x \in s$.
More concisely: For any additive group `α` and subset `s`, an element `x` belongs to the coset `a + s` if and only if `x` is congruent to an element in `s` modulo `a`, i.e., `x ≡ s (mod a)`.
|
Mathlib.GroupTheory.Coset._auxLemma.2
theorem Mathlib.GroupTheory.Coset._auxLemma.2 :
∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), (x ∈ a • s) = (a⁻¹ * x ∈ s)
This theorem, called `Mathlib.GroupTheory.Coset._auxLemma.2`, states that for any type `α` that forms a group (denoted by `[inst : Group α]`), given a set `s` of elements of type `α` and any elements `x` and `a` of type `α`, the element `x` is in the left coset of `s` by `a` (denoted by `a • s`), if and only if the product of the inverse of `a` and `x` (denoted by `a⁻¹ * x`) is in the set `s`. In the context of group theory, this theorem provides a condition for membership in a coset.
More concisely: For any group `α` and `s ∈ α`, `x ∈ α`, an element `x` belongs to the left coset `s` under `a ∈ α` if and only if `a⁻¹ * x ∈ s`.
|
QuotientGroup.eq'
theorem QuotientGroup.eq' : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {a b : α}, ↑a = ↑b ↔ a⁻¹ * b ∈ s := by
sorry
This theorem, `QuotientGroup.eq'`, states that for any type `α` that forms a group, given a subgroup `s` of α and any two elements `a` and `b` of α, the quotient of `a` and `b` are equal if and only if the product of the inverse of `a` and `b` is an element of the subgroup `s`. This theorem uses the equivalence between two conditions: equality in the quotient group and belonging to a certain subgroup in the original group.
More concisely: For any group `α` and subgroup `s`, two elements `a` and `b` of `α` are equivalent in the quotient group if and only if the product of the inverse of `a` and `b` belongs to `s`.
|
QuotientGroup.leftRel_eq
theorem QuotientGroup.leftRel_eq :
∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ s
This theorem states that for any type `α` that forms a group (i.e., satisfies the group axioms), and for any subgroup `s` of this group, the equivalence relation `Setoid.r` is defined as the property that the product of the inverse of `x` and `y` belongs to the subgroup `s`. In other words, two elements `x` and `y` of the group are considered equivalent under this relation if and only if their ratio `x⁻¹ * y` is an element of the subgroup `s`.
More concisely: For any group `α` and subgroup `s`, elements `x` and `y` are equal up to the subgroup `s` if and only if `x⁻¹ * y` belongs to `s`.
|
Mathlib.GroupTheory.Coset._auxAddLemma.3
theorem Mathlib.GroupTheory.Coset._auxAddLemma.3 :
∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), (x ∈ AddOpposite.op a +ᵥ s) = (x + -a ∈ s) := by
sorry
This theorem is a statement about additive groups and sets in the context of group theory. For any type `α` that forms an additive group, any set `s` of elements of `α`, any element `x` of `α`, and any element `a` of `α`, it states that `x` is an element of the set obtained by adding the opposite of `a` (`AddOpposite.op a`) to every element of `s` (denoted `AddOpposite.op a +ᵥ s`) if and only if the result of adding the additive inverse of `a` to `x` (denoted `x + -a`) is an element of `s`. The `+ᵥ` operation signifies a translation of the set `s` by the element `AddOpposite.op a`. In simple terms, the theorem states that translating a set by some element is equivalent to translating the element by its opposite in the opposite direction.
More concisely: For any additive group `α`, set `s` of elements in `α`, and element `a` in `α`, the set `s` and `AddOpposite.op a + s` (translation of `s` by `AddOpposite.op a`) are equal if and only if `x + -a` is an element of `s` for all `x` in `s`.
|
Subgroup.card_subgroup_dvd_card
theorem Subgroup.card_subgroup_dvd_card :
∀ {α : Type u_1} [inst : Group α] [inst_1 : Fintype α] (s : Subgroup α) [inst_2 : Fintype ↥s],
Fintype.card ↥s ∣ Fintype.card α
**Lagrange's Theorem** in group theory states that the order (number of elements) of a subgroup always divides the order of the larger (ambient) group to which it belongs. This theorem is applicable for finite groups, i.e., groups with a finite number of elements. In the Lean 4 theorem, `Subgroup.card_subgroup_dvd_card`, the order of the subgroup is represented by `Fintype.card ↥s` and the order of the ambient group is represented by `Fintype.card α`. The theorem asserts that the order of the subgroup divides (`∣`) the order of the ambient group for any group `α` and subgroup `s` of `α`.
More concisely: The order of a subgroup of a finite group divides the order of the group.
|
QuotientAddGroup.eq'
theorem QuotientAddGroup.eq' :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {a b : α}, ↑a = ↑b ↔ -a + b ∈ s
This theorem, named "QuotientAddGroup.eq'", states that for all elements `a` and `b` of an additive group `α`, and for a given additive subgroup `s` of `α`, the equivalence class of `a` is equal to the equivalence class of `b` if and only if the element obtained by adding the additive inverse of `a` to `b` belongs to the subgroup `s`. In other words, `a` and `b` are equivalent under the quotient group's equivalence relation precisely when their difference belongs to the subgroup `s`.
More concisely: For all additive groups α, subgroups s of α, and elements a, b in α, a ≡ b (mod s) if and only if a - b ∈ s.
|
leftCoset_eq_iff
theorem leftCoset_eq_iff :
∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s
This theorem states that for any given type `α` that forms a group and for any subgroup `s` of `α`, the left coset of `s` under `x` equals the left coset of `s` under `y` if and only if the element represented by the inverse of `x` times `y` is in `s`. In terms of group theory, it links the condition of two left cosets being equal to the existence of a certain element in the subgroup.
More concisely: For any group `α` and subgroup `s`, the left cosets `xs` and `ys` of `s` are equal if and only if `x⁻¹y ∈ s`.
|
QuotientGroup.mk_surjective
theorem QuotientGroup.mk_surjective :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α}, Function.Surjective QuotientGroup.mk
This theorem states that for any type `α` that has a group structure and any subgroup `s` of `α`, the canonical map from the group `α` to the quotient group `α ⧸ s`, denoted by `QuotientGroup.mk`, is surjective. In other words, every element in the quotient group `α ⧸ s` is the image of some element from the group `α` under the `QuotientGroup.mk` map.
More concisely: For any group `α` and subgroup `s`, the canonical quotient map `QuotientGroup.mk : α → α / s` is surjective.
|
QuotientAddGroup.eq
theorem QuotientAddGroup.eq :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {a b : α}, ↑a = ↑b ↔ -a + b ∈ s
This theorem states that for all types `α` of an additive group, given an additive subgroup `s` of `α` and any two elements `a` and `b` of `α`, the equivalence class of `a` is equal to the equivalence class of `b` if and only if the additive inverse of `a` plus `b` belongs to the subgroup `s`. In mathematical notation, this theorem says that for all `a, b` in `α` and a subgroup `s`, `a ~ b` in the quotient group iff `-a + b ∈ s`.
More concisely: For all types `α` of an additive group, two elements `a` and `b` belong to the same equivalence class in the quotient group if and only if the additive inverse of `a` plus `b` is in the subgroup.
|
QuotientGroup.induction_on'
theorem QuotientGroup.induction_on' :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x := by
sorry
This theorem, `QuotientGroup.induction_on'`, is a principle of mathematical induction for quotient groups in the context of group theory. Specifically, for any type `α` equipped with a group structure, and any subgroup `s` of `α`, it states that if a property `C` holds for every element `z` of the original group when considered as an element of the quotient group (that is, `C ↑z`), then `C` holds for every element `x` in the quotient group `α ⧸ s`.
More concisely: If `C` is a property that holds for every coset `[x]` of a subgroup `s` in a group `α`, then `C` holds for every element `x` in `α` (in the quotient group `α ⧸ s`).
|
QuotientAddGroup.leftRel_eq
theorem QuotientAddGroup.leftRel_eq :
∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => -x + y ∈ s
This theorem states that for any given type `α` that forms an additive group, and any additive subgroup `s` of this additive group, the distinguished equivalence relation of a setoid (`Setoid.r`) is defined as the relation where the result of subtracting `y` from the negation of `x` belongs to the subgroup `s`. In more mathematical terms, `-x + y ∈ s`.
More concisely: For any additive group `α` and subgroup `s`, the setoid equality `x ≈ y` holds if and only if `x - y ∈ s`.
|
QuotientAddGroup.mk_add_of_mem
theorem QuotientAddGroup.mk_add_of_mem :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {b : α} (a : α), b ∈ s → ↑(a + b) = ↑a
This theorem states that for any given type `α` which has an `AddGroup` structure, and for any given add subgroup `s` of `α`, and for any element `b` of `α`, if `b` is in `s`, then the additive quotient group element of `a + b` is equal to the quotient group element of `a`. Here, `a` and `b` are elements of `α`, `s` is an additive subgroup of `α`, and the ↑ operator is used to represent the natural projection from `α` to the quotient group `α/s`.
More concisely: If `α` is a type with an AddGroup structure, `s` is an additive subgroup of `α`, and `b` is an element of `α` in `s`, then `↑(a + b) = ↑a` for all `a` in `α`.
|
mem_rightCoset_iff
theorem mem_rightCoset_iff :
∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ MulOpposite.op a • s ↔ x * a⁻¹ ∈ s
This theorem states that for any given type `α` that forms a Group, for any set `s` of elements of type `α`, and for any elements `x` and `a` of type `α`, `x` is in the right coset of `s` formed by multiplying `s` by the multiplicative opposite of `a` if and only if the result of multiplying `x` by the inverse of `a` is in `s`. In other words, it provides a condition to check if an element belongs to a particular right coset in a Group.
More concisely: For any group `α`, set `s ⊆ α`, element `a ∈ α`, and `x ∈ α`, `x ∈ s * (−a)` if and only if `x * a^−1 ∈ s`, where `*` denotes group multiplication and `^−1` denotes the multiplicative inverse.
|
Mathlib.GroupTheory.Coset._auxLemma.3
theorem Mathlib.GroupTheory.Coset._auxLemma.3 :
∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), (x ∈ MulOpposite.op a • s) = (x * a⁻¹ ∈ s) := by
sorry
The theorem, named `_auxLemma.3` from the `Mathlib.GroupTheory.Coset` module, states that for any type `α` that forms a group (denoted by `[inst : Group α]`), given a set `s` of elements of type `α`, and elements `x` and `a` of type `α`, the condition that `x` belongs to the set formed by applying the 'multiplication opposite operation' (`MulOpposite.op`) on `a` and then 'scaling' the set `s` (denoted by `MulOpposite.op a • s`), is equivalent to the condition that the product `x * a⁻¹` belongs to the set `s`. Here, `a⁻¹` represents the inverse of `a` in the group context.
More concisely: For any group `α` and set `s` of elements, an element `x` belongs to the set `MulOpposite.op a • s` if and only if `x * a⁻¹` is in `s`.
|
QuotientGroup.leftRel_apply
theorem QuotientGroup.leftRel_apply :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ s
This theorem establishes a relationship between the equivalence relation defined by a setoid and an element of a subgroup in the context of group theory. Specifically, for any type `α` equipped with a group structure, a subgroup `s` of `α`, and any two elements `x` and `y` from `α`, the theorem states that `x` is related to `y` under the setoid's equivalence relation if and only if the result of multiplying the inverse of `x` by `y` belongs to the subgroup `s`.
More concisely: For any group `α` with subgroup `s`, elements `x` and `y` from `α` are equivalent under the setoid's relation if and only if `s` contains the product of `x^(-1)` and `y`.
|
mem_leftCoset_iff
theorem mem_leftCoset_iff : ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a • s ↔ a⁻¹ * x ∈ s := by
sorry
This theorem, `mem_leftCoset_iff`, states that for any type `α` that forms a group and for any set `s` of elements from that group, a given element `x` is in the left coset of `s` under an element `a` if and only if the product of the inverse of `a` and `x` is in `s`. Here, the left coset of `s` under `a` is represented by `a • s` and the inverse of `a` is represented by `a⁻¹`. The product of the inverse of `a` and `x` is denoted by `a⁻¹ * x`. This provides a condition for membership in left cosets in group theory.
More concisely: For any group type `α` and set `s` of elements, an element `x` lies in the left coset `a • s` if and only if `a⁻¹ * x ∈ s`.
|
mem_rightAddCoset_iff
theorem mem_rightAddCoset_iff :
∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ AddOpposite.op a +ᵥ s ↔ x + -a ∈ s
This theorem states that for any type `α` which forms an additive group, any set `s` of elements from this type, any element `x` in `α`, and any element `a` in `α`, `x` belongs to the right coset formed by adding `a` to each element of `s` if and only if the element obtained by adding the additive inverse of `a` to `x` belongs to `s`. The '+' operation refers to the addition defined in the additive group, and 'ᵥ' is used to denote the operation of adding an element to every member of a set, forming a coset.
More concisely: For any additive group `α`, set `s ⊆ α`, element `x ∈ α`, and `a ∈ α`, `x ∈ s + a` if and only if `x - a ∈ s`.
|
QuotientAddGroup.mk_surjective
theorem QuotientAddGroup.mk_surjective :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α}, Function.Surjective QuotientAddGroup.mk
The theorem `QuotientAddGroup.mk_surjective` states that for every type `α` that has an `AddGroup` structure and for every additive subgroup `s` of `α`, the canonical map `QuotientAddGroup.mk` from `α` to the quotient group `α ⧸ s` is surjective. In other words, for every element in the quotient group `α ⧸ s`, there exists an element in `α` such that when the `QuotientAddGroup.mk` function is applied to this element, the original element from the quotient group is obtained.
More concisely: For every `AddGroup` type `α` and additive subgroup `s`, the canonical map from `α` to the quotient group `α / s` is surjective.
|
QuotientAddGroup.induction_on'
theorem QuotientAddGroup.induction_on' :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
This theorem, named `QuotientAddGroup.induction_on'`, is about induction on elements of the quotient of an Additive Group `α` by an Additive Subgroup `s`. It states that, given any type `α` which has an `AddGroup` structure, any Additive Subgroup `s` of `α`, and any property `C` that applies to elements of the quotient group `α ⧸ s`, if `C` holds for all representatives `z` of equivalence classes (i.e., for all `z` in `α`), then `C` must hold for any element `x` in the quotient group `α ⧸ s`.
More concisely: If `C` is a property that holds for the representatives of every equivalence class in the quotient group `α / s` of an additive group `α` by an additive subgroup `s`, then `C` holds for every element in the quotient group.
|
QuotientGroup.eq
theorem QuotientGroup.eq : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {a b : α}, ↑a = ↑b ↔ a⁻¹ * b ∈ s := by
sorry
This theorem states that for any group `α` and any subgroup `s` of `α`, two elements `a` and `b` of `α` are equivalent in the quotient group `α / s` if and only if the element obtained by multiplying the inverse of `a` with `b` belongs to the subgroup `s`. In mathematical terms, $a \sim b$ in the quotient group if and only if $a^{-1}b \in s$.
More concisely: In a group, two elements are equivalent in the quotient group if and only if their product with the inverse of one element belongs to the subgroup. ($a \sim b$ in the quotient group if and only if $a^{-1}b \in s$).
|
QuotientGroup.out_eq'
theorem QuotientGroup.out_eq' :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (a : α ⧸ s), ↑(Quotient.out' a) = a
The theorem `QuotientGroup.out_eq'` states that for any type `α` with a group structure (indicated by `inst : Group α`), and any subgroup `s` of `α`, and any element `a` of the quotient group `α ⧸ s`, applying the function `Quotient.out'` to `a` and then applying the embedding of `α` into the quotient group `α ⧸ s` (indicated by `↑`) gives back the original element `a`. In other words, the `Quotient.out'` function is a right inverse to the quotient map for quotient groups.
More concisely: For any group `α` and subgroup `s`, the `Quotient.out'` function on the quotient group `α ⧸ s` is a right inverse to the quotient map, i.e., `Quotient.out' (↑a) = a` for all `a` in `α ⧸ s`.
|
QuotientAddGroup.leftRel_apply
theorem QuotientAddGroup.leftRel_apply :
∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ -x + y ∈ s
This theorem states that for any type `α` which is an additive group, and any additive subgroup `s` of `α`, and any elements `x` and `y` of `α`, the relation `x ≈ y` (which is defined by the Setoid `r` on `α`) holds if and only if `-x + y` is an element of the subgroup `s`. In other words, in the context of quotient groups, two elements `x` and `y` from an additive group are equivalent (according to the equivalence relation defined by the Setoid) if their difference `-x + y` belongs to the given subgroup.
More concisely: For any additive group `α`, additive subgroup `s`, and elements `x` and `y` of `α`, `x ≈ y` if and only if `-x + y` is in `s`.
|
QuotientGroup.mk_mul_of_mem
theorem QuotientGroup.mk_mul_of_mem :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {b : α} (a : α), b ∈ s → ↑(a * b) = ↑a
This theorem, `QuotientGroup.mk_mul_of_mem`, states that for any type `α` that has a group structure, any subgroup `s` of `α`, and any two elements `a` and `b` of `α`, if `b` is a member of the subgroup `s`, then the quotient group element represented by `a * b` is equal to the quotient group element represented by `a`. In other words, multiplication by an element of the subgroup does not change the equivalence class in the quotient group, reflecting the effect of the normal subgroup on the group structure.
More concisely: For any group `α` and subgroup `s`, if `b ∈ s`, then `[a] : s → α / s = [a * b] : σ → α / s`, where `[a]` and `[a * b]` denote the quotient group elements represented by `a` and `a * b`, respectively.
|
AddSubgroup.card_addSubgroup_dvd_card
theorem AddSubgroup.card_addSubgroup_dvd_card :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : Fintype α] (s : AddSubgroup α) [inst_2 : Fintype ↥s],
Fintype.card ↥s ∣ Fintype.card α
**Lagrange's Theorem**: For any additive group `α` that has a finite number of elements, and for any additive subgroup `s` of `α` that also has a finite number of elements, the size of the subgroup `s` (denoted as `Fintype.card ↥s`) is a divisor of the size of the group `α` (denoted as `Fintype.card α`). In other words, the number of elements in the group is an integer multiple of the number of elements in the subgroup.
More concisely: For any finite additive group `α` and its finite subgroup `s`, the order of `s` divides the order of `α`.
|
QuotientGroup.rightRel_apply
theorem QuotientGroup.rightRel_apply :
∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ s
This theorem, "QuotientGroup.rightRel_apply", states that for any type `α` that has a group structure, given a subgroup `s` of `α` and any two elements `x` and `y` of `α`, `x` is related to `y` under the distinguished equivalence relation of the setoid if and only if the product of `y` and the inverse of `x` belongs to the subgroup `s`. This theorem ties the concept of equivalence relation to the algebraic structure of groups and subgroups.
More concisely: For any group `α` and subgroup `s`, `x ≃ y` if and only if `y * x^-1 ∈ s`, where `≃` denotes the equivalence relation on `α` induced by the subgroup `s`.
|