smul_apply_eq_smul_apply_inv_smul

English

The smul of the left-quotient equivalence commutes with inverse smul: applying smul with f on the left-quotient equvalent of q equals smul by f^{-1} on q's image.

Русский

Умножение слева на коэффициент f сопряжено с инверсией: применяя smul слева к эквивалентности leftQuotientEquiv, получим эквивалентность, соответствующую smul на q с f^{-1}.

LaTeX

$$$\\text{smul_leftQuotientEquiv}(f) \\, q = (f\\!^{-1} \\cdot q)\\;\\text{leftQuotientEquiv}$ (equational form via smul_inv_smul).$$

Lean4

@[to_additive]
theorem smul_apply_eq_smul_apply_inv_smul (f : F) (S : H.LeftTransversal) (q : G ⧸ H) :
    ((f • S).2.leftQuotientEquiv q : G) = f • (S.2.leftQuotientEquiv (f⁻¹ • q) : G) := by
  rw [smul_leftQuotientEquiv, smul_inv_smul]

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