English
The diff is invariant under the group action: applying the same group element g to both transversals does not change the diff: diff(ϕ,(g•S),(g•T)) = diff(ϕ,S,T).
Русский
Разность неизменна при одновременном действии группы: diff(ϕ,(g • S),(g • T)) = diff(ϕ,S,T).
LaTeX
$$$\operatorname{diff}(\varphi,(g\cdot S),(g\cdot T)) = \operatorname{diff}(\varphi,S,T)$$$
Lean4
@[to_additive]
theorem smul_diff_smul (g : G) : diff ϕ (g • S) (g • T) = diff ϕ S T :=
let _ := H.fintypeQuotientOfFiniteIndex
Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun _ ↦ by
simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left,
toPerm_symm_apply]