top_prod — Mathlib

English

The product of ⊤ in the first factor with K equals the comap along the second projection: (⊤ : Subgroup G).prod K = comap (snd) K.

Русский

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

LaTeX

$$$ (\top : \mathrm Subgroup G) . \mathrm{prod} K = \mathrm{comap}(\mathrm{snd}) K $$$

Lean4

@[to_additive top_prod]
theorem top_prod (H : Subgroup N) : (⊤ : Subgroup G).prod H = H.comap (MonoidHom.snd G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

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