English
A further variant expresses the same identity using orbitRel Quotients and alternative representatives.
Русский
Другая вариация выражает то же тождество через quotient по orbitRel и альтернативные представления.
LaTeX
$$$\uparrow\bigl((\mathrm{transferTransversal}(H,g)).2.leftQuotientEquiv (\text{something})\bigr) = \text{case split identity}$$$$
Lean4
theorem transferTransversal_apply'' (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
(k : ZMod (minimalPeriod (g • ·) q.out)) :
↑((g • transferTransversal H g).2.leftQuotientEquiv (g ^ (cast k : ℤ) • q.out)) =
if k = 0 then g ^ minimalPeriod (g • ·) q.out * q.out.out else g ^ (cast k : ℤ) * q.out.out :=
by
rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ← mul_smul, ← zpow_neg_one,
← zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc, ← zpow_one_add, Int.cast_add, Int.cast_neg,
Int.cast_one, intCast_cast, cast_id', id, ← sub_eq_neg_add, cast_sub_one, add_sub_cancel]
by_cases hk : k = 0
· rw [if_pos hk, if_pos hk, zpow_natCast]
· rw [if_neg hk, if_neg hk]
