inv_mul_toLeftFun_mem — Mathlib

English

For every g, if r = toLeftFun g is the chosen representative of the left coset gH, then r^{-1}g ∈ H.

Русский

Для каждого g, если r = toLeftFun g — выбранный представитель левого косета gH, то r^{-1}g ∈ H.

LaTeX

$$$\\forall g\\in G,\\; (toLeftFun\\, hS\\, g : G)^{-1} \\cdot g \\in H.$$$

Lean4

@[to_additive]
theorem inv_mul_toLeftFun_mem (hS : IsComplement S H) (g : G) : g⁻¹ * toLeftFun hS g ∈ H :=
  (congr_arg (· ∈ H) (by rw [mul_inv_rev, inv_inv])).mp (H.inv_mem (inv_toLeftFun_mul_mem hS g))

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