embedProduct_injective — Mathlib

English

The map embedProduct is injective for any α with a monoid structure.

Русский

Отображение embedProduct инъективно для любой моноидной структуры α.

LaTeX

$$$\\mathrm{embedProduct}: \\mathrm{Units}(\\alpha) \\to \\alpha \\times \\alpha^{\\mathrm{op}}\\text{ инъективно}$$$

Lean4

@[to_additive]
theorem embedProduct_injective (α : Type*) [Monoid α] : Function.Injective (embedProduct α) := fun _ _ h =>
  Units.ext <| (congr_arg Prod.fst h :)

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