English
If H has finite index, then H is finitely generated by a Schreier-type argument.
Русский
Если индекс H конечен, то H конечносгенерируема.
LaTeX
$$instance FG (H) : Group.FG H$$
Lean4
theorem smul_diff' (h : H) : diff (MonoidHom.id H) α (op (h : G) • β) = diff (MonoidHom.id H) α β * h ^ H.index :=
by
letI := H.fintypeQuotientOfFiniteIndex
rw [diff, diff, index_eq_card, Nat.card_eq_fintype_card, ← Finset.card_univ, ← Finset.prod_const, ←
Finset.prod_mul_distrib]
refine Finset.prod_congr rfl fun q _ => ?_
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, MulOpposite.unop_op, mul_left_inj, ← Subtype.ext_iff,
Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
exact left_eq_mul.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)
