eq_one_iff — Mathlib

English

The composition of mk' N with the subtype map N → G is the trivial map sending every element of N to the identity coset 1.

Русский

Композиция mk' N с включением из N в G является тождественно нулевой на N, т.е. отправляет каждый элемент N в единичный косет.

LaTeX

$$((mk' N) ∘ N.subtype) = 1$$

Lean4

@[to_additive (attr := simp)]
theorem eq_one_iff {N : Subgroup G} [N.Normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N :=
  by
  refine QuotientGroup.eq.trans ?_
  rw [mul_one, Subgroup.inv_mem_iff]

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