equivOp — Mathlib

English

There is a natural equivalence between a subgroup H of G and its opposite H.op, given by the construction Subgroup.equivOp.

Русский

Существует естественная биекция между подгруппой H в G и её противоположностью H.op, задаваемая конструктором Subgroup.equivOp.

LaTeX

$$Subgroup.equivOp : H \to H.op is an equivalence$$

Lean4

/-- Bijection between a subgroup `H` and its opposite. -/
@[to_additive (attr := simps!) /-- Bijection between an additive subgroup `H` and its opposite. -/
    ]
def equivOp (H : Subgroup G) : H ≃ H.op :=
  MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl

Похожие утверждения