English
For a monoid α, the range of embedProduct α is the set of pairs (a, b) ∈ α × αᵐᵒᵖ such that a · unop b = 1 and unop b · a = 1.
Русский
Для моноида α область значений embedProduct α состоит из пар (a, b) ∈ α × αᵐᵒᵖ таких, что a · unop b = 1 и unop b · a = 1.
LaTeX
$$$ \\operatorname{range}(\\text{embedProduct } \\alpha) = \\{ p: \\alpha \\times \\alpha^{\\mathrm{op}} \\mid p_1 \\cdot \\mathrm{unop}(p_2) = 1 \\wedge \\mathrm{unop}(p_2) \\cdot p_1 = 1 \\} $$$
Lean4
@[to_additive]
theorem range_embedProduct [Monoid α] :
Set.range (embedProduct α) = {p : α × αᵐᵒᵖ | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1} :=
Set.range_eq_iff _ _ |>.mpr ⟨fun a ↦ ⟨a.mul_inv, a.inv_mul⟩, fun p hp ↦ ⟨⟨p.1, unop p.2, hp.1, hp.2⟩, rfl⟩⟩
