comap_map_mk' — Mathlib

English

If the quotient of a group by the trivial subgroup is a singleton, then the subgroup is the whole group.

Русский

Если фактор-группа по тривиальной подгруппе единична, то подгруппа равна всей группе.

LaTeX

$$$(G)/(\\top) \\text{ is a singleton }\\Rightarrow G = \\top$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_map_mk' (N H : Subgroup G) [N.Normal] : Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H := by
  simp [Subgroup.comap_map_eq, sup_comm]

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