stabilizerMulEquiv_apply

Mathlib.GroupTheory.Perm.DomMulAct

URI: https://scilib.ai/kg/mathlib#DomMulAct.stabilizerMulEquiv_apply

← MathLib Explorer

English

The square of a three-cycle is again a three-cycle.

Русский

Квадрат трёхцикла снова является трёхциклом.

LaTeX

$$IsThreeCycle(g) ⇒ IsThreeCycle(g^2)$$

Lean4

theorem stabilizerMulEquiv_apply (g : (stabilizer (Perm α)ᵈᵐᵃ f)ᵐᵒᵖ) {a : α} {i : ι} (h : f a = i) :
    ((stabilizerMulEquiv f)) g i ⟨a, h⟩ = (mk.symm g.unop : Equiv.Perm α) a :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru