toSubmonoid_injective — Mathlib

English

The map sending a subgroup to its underlying submonoid is injective.

Русский

Отображение, отправляющее подгруппу в ее соответствующий подмонойд, инъективно.

LaTeX

$$$\\text{toSubmonoid}: \\text{Subgroup}(G) \\to \\text{Submonoid}(G) \\text{ is injective}$$$

Lean4

@[to_additive]
theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) := fun p q h =>
  by
  have := SetLike.ext'_iff.1 h
  rw [coe_toSubmonoid, coe_toSubmonoid] at this
  exact SetLike.ext'_iff.2 this

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