English
The scalar action commutes with the left-transversal representative map: smul f on the representative corresponds to smul f on the input coset.
Русский
Действие скаляра сохраняется через отображение левого трансверсала.
LaTeX
$$$\\text{smul_toLeftFun}(f) \\, (S: H.LeftTransversal) = \\text{toLeftFun}(f • S)\\;.$$$
Lean4
@[to_additive]
theorem smul_toLeftFun (f : F) (S : H.LeftTransversal) (g : G) :
(f • (S.2.toLeftFun g : G)) = (f • S).2.toLeftFun (f • g) :=
Subtype.ext_iff.mp <|
@ExistsUnique.unique (↥(f • (S : Set G))) (fun s => (↑s)⁻¹ * f • g ∈ H)
(isComplement_iff_existsUnique_inv_mul_mem.mp (f • S).2 (f • g))
⟨f • (S.2.toLeftFun g : G), Set.smul_mem_smul_set (Subtype.coe_prop _)⟩ ((f • S).2.toLeftFun (f • g))
(QuotientAction.inv_mul_mem f (S.2.inv_toLeftFun_mul_mem g)) ((f • S).2.inv_toLeftFun_mul_mem (f • g))
