stabilizerHom_apply — Mathlib

English

For g in the stabilizer and b in B, the stabilizer-induced automorphism sends the class of b to the class of g·b.

Русский

Для g из стабилизатора и b из B отображение, индуцированное стабилизатором, отправляет класс b в класс g·b.

LaTeX

$$$\text{stabilizerHom }(g)(b) = g·b$ in the quotient$$

Lean4

@[simp]
theorem stabilizerHom_apply (g : MulAction.stabilizer G P) (b : B) : stabilizerHom P p G g b = ↑(g • b) :=
  rfl

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