English
If N is unique, then M × N ≃* M; i.e., multiplication by the trivial left factor leaves the monoid unchanged up to isomorphism.
Русский
Если N уникален, то M × N ≃* M; то есть умножение слева тривиционного фактора не меняет моноид до изоморфизма.
LaTeX
$$$[Unique N] \\Rightarrow M \\times N \\cong_* M$$$
Lean4
/-- Multiplying by the trivial monoid doesn't change the structure.
This is the `MulEquiv` version of `Equiv.prodUnique`. -/
@[to_additive prodUnique /-- Multiplying by the trivial monoid doesn't change the structure.
This is the `AddEquiv` version of `Equiv.prodUnique`. -/
]
def prodUnique [Unique N] : M × N ≃* M :=
{ Equiv.prodUnique M N with map_mul' := fun _ _ => rfl }
