coe_comapOfKerIsPGroup — Mathlib

English

The underlying subgroup of the Sylow obtained by comap_of_ker_isPGroup equals the comap of the original subgroup; the two are identified at the Subgroup level.

Русский

Основанная подгруппа Силова, полученная через comap_of_ker_isPGroup, совпадает с comap-образом исходной подгруппы.

LaTeX

$$$ (P.comapOfKerIsPGroup \\varphi h\\_\\u03c6 h).toSubgroup = (P.comap \\varphi).toSubgroup $$$

Lean4

@[simp]
theorem coe_comapOfKerIsPGroup (hϕ : IsPGroup p ϕ.ker) (h : P ≤ ϕ.range) : P.comapOfKerIsPGroup ϕ hϕ h = P.comap ϕ :=
  rfl

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