mul_inv_toRightFun_mem — Mathlib

English

If H is finite index and S forms a left complement with H, then the encard of S equals the index of H in G.

Русский

Если индекс H конечен и S образует левый комплемент с H, то encard S равно индексам H в G.

LaTeX

$$$[H\\text{ finite index}]\\; \\text{IsComplement } S H \\Rightarrow S.encard = H.index$$$

Lean4

@[to_additive]
theorem mul_inv_toRightFun_mem (hT : IsComplement H T) (g : G) : g * (toRightFun hT g : G)⁻¹ ∈ H :=
  QuotientGroup.rightRel_apply.mp <| Quotient.exact' <| mk''_rightQuotientEquiv _ _

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