定理陈述 #

设$H$和$K$是群$G$的有限子群，则$|HK|=\frac{|H||K|}{|H\cap K|}$。

你的证明细节正确性验证 #

整体来看，你填充的证明细节逻辑是通顺且核心思路正确的，只有步骤(4)的推导有一处可以优化得更严谨，我帮你梳理一下：

步骤(4)的推导优化 #

你假设$Hk_i \cap Hk_j \neq \emptyset$后，利用陪集的性质得出$Hk_i = Hk_j$，这个起点是对的，但后续的等式链可以更流畅：
假设$Hk_i = Hk_j$，则$k_i k_j^{-1} \in H$；又因为$k_i,k_j \in K$，所以$k_i k_j^{-1} \in K$，因此$k_i k_j^{-1} \in H\cap K = C$，这直接意味着$Ck_i = Ck_j$——但这和我们一开始把$K$分解为$C$的不相交右陪集$Ck_1 \cup \dots \cup Ck_n$矛盾（$i\neq j$时$Ck_i$与$Ck_j$本应无交集）。

你原推导里的等式链可以修正为：
$$
\begin{align}
Ck_i \cap Ck_j &= (H\cap K)k_i \cap (H\cap K)k_j \
&= (Hk_i \cap K) \cap (Hk_j \cap K) \quad \text{（对任意}b\in K\text{，}(H\cap K)b = Hb \cap Kb = Hb \cap K\text{）} \
&= (Hk_i \cap Hk_j) \cap K \
&= Hk_i \cap K \quad \text{（因为假设}Hk_i=Hk_j\text{）} \
&= Ck_i
\end{align}
$$
而$i\neq j$时$Ck_i \cap Ck_j = \emptyset$，但$k_i \in Ck_i$，这就产生了矛盾。你的核心逻辑没问题，只是推导过程可以避免跳步，让逻辑更连贯。

其余步骤(1)-(3)都是完全严谨的：

• 步骤(1)利用有限群子群指数有限的性质，明确了陪集分解的个数$n$，为后续计数打下基础；
• 步骤(2)通过双向包含的方法，扎实证明了$HC=H$，这是连接$H$与$K$陪集分解的关键桥梁；
• 步骤(3)对集合运算分配律的通用证明，为$HK$的陪集分解提供了可靠的理论依据。

定理的学习动机 #

特别理解你花几周没进展的挫败感——这个定理初看抽象，但它是有限群计数问题的核心工具，动机其实非常接地气：

1. 修正"重复计数"的直觉误差 #

直觉上你可能会觉得$|HK|=|H|\times|K|$，但实际上$H$和$K$的交集$H\cap K$里的元素会被重复计算：比如每个$c\in H\cap K$，在$H$里算一次，在$K$里又算一次，导致$HK$里的元素被多算了$|H\cap K|$次。这个定理本质就是在量化并修正这个重复计数的误差。

2. 为后续核心定理铺路 #

这个公式是群论后续很多重要结论的基础：

• Sylow定理的证明会用到类似的计数技巧；
• 当$HK$本身是子群时（比如$H$与$K$可交换，或其中一个是正规子群），用这个公式能快速计算$HK$的阶，进而分析群的结构；
• 它还能辅助判断$HK$是否为子群：若$\frac{|H||K|}{|H\cap K|}$整除$|G|$，结合其他条件就能推出$HK$是子群。

3. 训练"分解-计数"的核心思维 #

这个定理的证明核心是用陪集分解把复杂集合拆成不相交的简单单元，这种"拆解问题、逐个计数"的思路是有限群论的核心技巧。学会这个定理，本质是在训练你如何把看似混乱的集合（比如$HK$）转化为可计算的、清晰的结构，这种思维在后续群论学习中会反复用到。

备注：内容来源于stack exchange，提问作者user264745