English
Let G be a group and H ≤ G. The opposite subgroup H^{op} of the opposite group G^{op} is defined by H^{op} := { g^{op} ∈ G^{op} : g ∈ H }. The subgroup axioms are inherited from H, so H^{op} is a subgroup of G^{op}. In particular, 1 ∈ H^{op}, (ab)^{op} ∈ H^{op} whenever a^{op}, b^{op} ∈ H^{op}, and (a^{op})^{-1} ∈ H^{op} when a^{op} ∈ H^{op}.
Русский
Пусть G — группа и H ≤ G. Противоположная подгруппа H^{op} противоположной группы G^{op} задаётся как H^{op} := { g^{op} ∈ G^{op} : g ∈ H }. Группа-условия подгруппы наследуются от H, поэтому H^{op} является подгруппой G^{op}. В частности, единица принадлежит H^{op}, произведение двух элементов из H^{op} принадлежует H^{op}, и обратный элемент также лежит в H^{op}.
LaTeX
$$$H^{\mathrm{op}} \\le G^{\mathrm{op}}$$$
Lean4
/-- Pull a subgroup back to an opposite subgroup along `MulOpposite.unop` -/
@[to_additive (attr := simps) /--
Pull an additive subgroup back to an opposite additive subgroup along `AddOpposite.unop` -/
]
protected def op (H : Subgroup G) : Subgroup Gᵐᵒᵖ
where
carrier := MulOpposite.unop ⁻¹' (H : Set G)
one_mem' := H.one_mem
mul_mem' ha hb := H.mul_mem hb ha
inv_mem' := H.inv_mem
