English
From x ∈ S.ofUnits define a unit u ∈ M^× with u.val = x.
Русский
Из x ∈ S.ofUnits определяется единица u ∈ M^× такая, что u.val = x.
LaTeX
$$$ S.unit_of_mem_ofUnits h : M^{\times} $ with $ (S.unit_of_mem_ofUnits h).val = x $$$
Lean4
/-- Given some `x : M` which is a member of the submonoid of unit elements corresponding to a
subgroup of units, produce a unit of `M` whose coercion is equal to `x`. -/
@[to_additive /-- Given some `x : M` which is a member of the additive submonoid of additive unit
elements corresponding to a subgroup of units, produce a unit of `M` whose coercion is equal to
`x`. -/
]
noncomputable def unit_of_mem_ofUnits (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) : Mˣ :=
(Classical.choose h).copy x (Classical.choose_spec h).2.symm _ rfl
