of — Mathlib · SciLib

English

There is a canonical surjective homomorphism from G onto its abelianization, called the natural projection, sending each element to its class modulo the commutator subgroup.

Русский

Существует канонический сюръективный гомоморфизм G → Abelianization(G), называемый естественной проекцией, отправляющий элемент в его класс по модулю коммутаторов.

LaTeX

$$$$ \\mathrm{of} : G \\twoheadrightarrow \\mathrm{Abelianization}(G). $$$$

Lean4

/-- `of` is the canonical projection from G to its abelianization. -/
def of : G →* Abelianization G where
  toFun := QuotientGroup.mk
  map_one' := rfl
  map_mul' _ _ := rfl

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