op_unop — Mathlib

English

Same mutual inverse relationship as in 11148: the two maps op and unop are inverses of each other on subgroups.

Русский

Та же взаимная обратность: операции op и unop являются взаимно обратными на подгруппах.

LaTeX

$$$\text{op}\circ \text{unop} = \mathrm{id}$ и $\text{unop}\circ \text{op} = \mathrm{id}$ on Subgroup G$$

Lean4

@[to_additive (attr := simp)]
theorem op_unop (S : Subgroup Gᵐᵒᵖ) : S.unop.op = S :=
  rfl

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