smul_leftQuotientEquiv — Mathlib

English

The map smul on the left-quotient equivalence is compatible with the action: smul by f on the left-quotient representative equals the left-quotient of the smul by f on the coset q.

Русский

Совместимость действия слева с отображением левохКвази: умножение слева на представителе эквивалентности эквивалентно левому квази для косета.

LaTeX

$$$\\forall f, S, q,\\; f \\cdot (S.2.leftQuotientEquiv q) = (f \\cdot S).2.leftQuotientEquiv (f \\cdot q)$$$

Lean4

@[to_additive]
theorem smul_leftQuotientEquiv (f : F) (S : H.LeftTransversal) (q : G ⧸ H) :
    f • (S.2.leftQuotientEquiv q : G) = (f • S).2.leftQuotientEquiv (f • q) :=
  Quotient.inductionOn' q fun g => smul_toLeftFun f S g

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