coe_comapOfInjective — Mathlib

English

The equality of the underlying subgroups holds: the Sylow obtained by comap_of_injective has the same underlying subgroup as comap φ of P.

Русский

Равенство основанных подгрупп: подпогруппа Силова, полученная через comap_of_injective, имеет ту же основанную подгруппу, что и comap φ от P.

LaTeX

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

Lean4

@[simp]
theorem coe_comapOfInjective (hϕ : Function.Injective ϕ) (h : P ≤ ϕ.range) : P.comapOfInjective ϕ hϕ h = P.comap ϕ :=
  rfl

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