equiv_snd_eq_inv_mul — Mathlib

English

With φ(s,t) = s t, the second component satisfies t = s^{-1} g wherever g = s t with s ∈ S, t ∈ T; equivalently, t = s^{-1} g.

Русский

При разложении g = s t с s ∈ S, t ∈ T, второй компонент равен t = s^{-1} g; иными словами, t = s^{-1} g.

LaTeX

$$$\forall g\in G:\; \exists! (s,t)\in S\times T:\; g=s t\Rightarrow t = s^{-1} g.$$$

Lean4

theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst : G)⁻¹ * g :=
  eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g)

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