orbit — Mathlib

English

For H ⊲ G, the action of g on h ∈ H is given by g h g^{-1}. This is the conjunction defining the map g ↦ inner automorphism of H.

Русский

Для H ⊲ G действие g на h ∈ H задается как g h g^{-1}. Это определение отображения g в внутренний автоморфизм H.

LaTeX

$$$↑(MulAut.conjNormal g h) = g h g^{-1}$$$

Lean4

/-- The orbit of an element under an action. -/
@[to_additive /-- The orbit of an element under an action. -/
    ]
def orbit (a : α) :=
  Set.range fun m : M => m • a

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