mk'_eq_mk' — Mathlib

English

For x,y in G, mk' N x = mk' N y if and only if there exists z in N such that xz = y.

Русский

Для x,y в G верно: косет xN равен косету yN тогда и только тогда, когда существует z ∈ N такое, что xz = y.

LaTeX

$$$(\\text{mk}'\\ N\\ x) = (\\text{mk}'\\ N\\ y) \\iff \\exists z \\in N,\\ xz = y$$$

Lean4

@[to_additive]
theorem mk'_eq_mk' {x y : G} : mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y :=
  QuotientGroup.eq.trans <| by simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_eq_right]

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