prod_top — Mathlib

English

The product of a subgroup K with the top subgroup ⊤ in the second factor equals the comap of K along the first projection: K.prod (⊤) = comap (fst) K.

Русский

Произведение подгруппы K с верхней ⊤ во втором факторе равно прообразу K по проекции fst: K.prod(⊤) = comap(fst) K.

LaTeX

$$$ K \mathrm{prod} (\top : \mathrm Subgroup N) = K.\mathrm{comap}(\mathrm{fst}) $$$

Lean4

@[to_additive prod_top]
theorem prod_top (K : Subgroup G) : K.prod (⊤ : Subgroup N) = K.comap (MonoidHom.fst G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

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