mk' — Mathlib

English

The canonical embedding mk' from G to G/N corresponds to the quotient map mk, i.e., mk' equals mk in the appropriate sense.

Русский

Каноническое вложение mk' из G в G/N совпадает с mk в соответствующем смысле.

LaTeX

$$$(mk' N) = mk$$$

Lean4

/-- The group homomorphism from `G` to `G/N`. -/
@[to_additive /-- The additive group homomorphism from `G` to `G/N`. -/
    ]
def mk' : G →* G ⧸ N :=
  MonoidHom.mk' QuotientGroup.mk fun _ _ => rfl

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