smul_diff_smul — Mathlib

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]

Похожие утверждения