English
Let F be a type equipped with an equivalence-like structure between α and β, with Mul on α and β. The map that sends an element of F to its corresponding multiplicative equivalence α ≃* β is injective; equivalently, if e1 and e2 in F have the same underlying multiplicative equivalence, then e1 = e2.
Русский
Пусть F — множество с структурой эквивалентности между α и β, над которыми задано умножение. Отображение элемента F в соответствующее умножительное эквивалентство α ≃* β инъективно; то есть если e1 и e2 в F имеют одинаковое основание в виде эквивалентности, то e1 = e2.
LaTeX
$$$\operatorname{Injective}\bigl( (\uparrow) : F \to (\alpha \simeq^* \beta) \bigr)$$$
Lean4
@[to_additive]
theorem toMulEquiv_injective [Mul α] [Mul β] [MulEquivClass F α β] : Function.Injective ((↑) : F → α ≃* β) :=
fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
