----
> [!theorem] Theorem. ([[Lagrange's Theorem]])
> If $H \subset G$ is a [[subgroup]] of a finite [[group]] $G$, then $|H|$ [[divides]] $|G|$ because $|G|=|H|[G:H]$.
> \
> **Remark.** All of the lemmas below should be visually clear from the [[Cayley diagram]] interpretation of [[coset]]s.
> [!proposition] Lemma 1. (Cosets are either identical or disjoint)
> **Proof of Lemma 1.** We'll do the left coset case; right coset case is similar. Let $H \leq G$; $a,b \in G$. Suppose *non-disjointness*: $aH \cap bH \neq \emptyset$. Then there exists an element $c$ in these [[coset|left cosets']] intersection having the form $c=ah_{1}=bh_{2}$
for some $h_{1},h_{2} \in H$. Observe that since $a=b(h_{2}h_{1} ^{-1}) \in bH,$
we must have *identicality*: $aH=bH$ .
> [!proposition] Lemma 2. (All cosets have the same [[cardinality]])
> **Proof of Lemma 2.** Again, we'll do the left coset case. Let $H \leq G$ and take $a \in G$. Define $f:H\to aH$ given by $f(x)=ax$. $f$ is [[surjection|surjective]] by construction, and if $f(x)=ax=ay=f(y)$ then $x=y$ by cancellation. So $f$ is [[injection|injective]], hence a [[bijection]]. Thus $|eH|=|aH|$ for all $a \in G$.
>
^f23554
> [!proposition] Lemma 3. ([[coset|cosets]] [[partition]] [[group]])
> **Proof of Lemma 3.** We'll do left cosets as usual. We need to show that for all $a \in G$, there exists a coset containing $a$. Via **lemma 1** it suffices to show $G=\cup \text{(left cosets)}$. Pick $a\in G$, then $a=ae \in aH \in (\text{left cosets)}$.
> ![[CleanShot 2023-09-05 at
[email protected]]]
> [!proof]- Proof. ([[Lagrange's Theorem]])
> Suppose there are $n$ [[coset|left cosets]] of $H$. Since they are all the same size (**lemma 2**) — namely $|H|$— and they partition $G$ (**lemmas 1/3**), we must have $|G|= \overbrace{|H|+\dots+|H|}^{n \text{copies}}=n|H|.$
> I.e., we see that $|G|=|H|\cdot (\text{number of left cosets})=|G|[G:H].$
----
####
-----
#### References
> [!backlink]
> ```dataview
TABLE rows.file.link as "Further Reading"
FROM [[]]
FLATTEN file.tags
GROUP BY file.tags as Tag
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```