mem_fixedBy

Mathlib.GroupTheory.GroupAction.Defs

URI: https://scilib.ai/kg/mathlib#MulAction.mem_fixedBy

English

For each m ∈ M, a ∈ α is in fixedBy α m exactly when m • a = a.

Русский

Для каждого m ∈ M a ∈ α принадлежит fixedBy α m тогда, когда m • a = a.

LaTeX

$$$$ a \\in fixedBy(\\alpha, m) \\iff m \\cdot a = a. $$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_fixedBy {m : M} {a : α} : a ∈ fixedBy α m ↔ m • a = a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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