mk_out_eq_mul — Mathlib

English

For any element g of the ambient group, there exists h in s such that the coset mk g is represented by g · h.

Русский

Для любого элемента g в группе существует h ∈ s, так что косет mk g задаётся представителем g · h.

LaTeX

$$$\exists h \in s, \; (\text{mk } g) = g \cdot h$$$

Lean4

@[to_additive QuotientAddGroup.mk_out_eq_mul]
theorem mk_out_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h :=
  ⟨⟨g⁻¹ * (mk g).out, QuotientGroup.eq.mp (mk g).out_eq'.symm⟩, by rw [mul_inv_cancel_left]⟩

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