subtype — Mathlib

English

A Sylow p-subgroup of G yields a Sylow p-subgroup of any subgroup N of G, provided by the subtype embedding.

Русский

Подпогруппа Силова p G порождает подпогруппу Силова p N для любой подгруппы NG, через вложение subtype.

LaTeX

$$$ (h : P ≤ N) \\Rightarrow P.subtype h \\text{ is a Sylow } p N$$

Lean4

/-- A sylow subgroup of G is also a sylow subgroup of a subgroup of G. -/
protected def subtype (h : P ≤ N) : Sylow p N :=
  P.comapOfInjective N.subtype Subtype.coe_injective (by rwa [range_subtype])

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