toCommMonoid_injective — Mathlib

English

The forgetful map from CancelCommMonoid to CancelMonoid is injective.

Русский

Отображение CancelCommMonoid в CancelMonoid инъективно.

LaTeX

$$$\text{toCommMonoid}$ is injective for CancelCommMonoid: equal underlying commutative multiplication implies equality.$$

Lean4

@[to_additive]
theorem toCommMonoid_injective {M : Type u} : Function.Injective (@CancelCommMonoid.toCommMonoid M) :=
  by
  rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h
  grind

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