toMulEquiv_injective — Mathlib

English

The map that sends an ordered monoid isomorphism to its underlying multiplicative equivalence is injective.

Русский

Отображение, отправляющее упорядоченный моноидный изоморфизм на эквивалентность умножения, инъективно.

LaTeX

$$$Injective\left(toMulEquiv : _ \to α \simeq^* β\right).$$$

Lean4

@[to_additive]
theorem toMulEquiv_injective : Injective (toMulEquiv : _ → α ≃* β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

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