quotientGroupMk_leftQuotientEquiv

English

For a given complement hS of S and H, the left quotient equivalence respects quotient representatives: the quotient map of the chosen representative equals the underlying quotient.

Русский

Для данного дополнения hS группы S и подгруппы H, лево-возмущающая эквивалентность сохраняет представления косета: отображение к квоти соединяет выбранного представителя и базовый фактор.

LaTeX

$$$ Quotient.mk'' (leftQuotientEquiv hS q : G) = q $$$

Lean4

@[to_additive]
theorem quotientGroupMk_leftQuotientEquiv (hS : IsComplement S H) (q : G ⧸ H) :
    Quotient.mk'' (leftQuotientEquiv hS q : G) = q :=
  hS.leftQuotientEquiv.symm_apply_apply q

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