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