map_toSubmonoid — Mathlib

English

Equality of underlying submonoids induced by a subgroup map holds by reflexivity of the construction.

Русский

Равенство подмножества подгруппы, индуцированное отображением, следует из фиксации конструкции.

LaTeX

$$$ (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid $$$

Lean4

@[to_additive (attr := simp)]
theorem map_toSubmonoid (f : G →* G') (K : Subgroup G) :
    (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid :=
  rfl

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