fixedBy_one_eq_univ

Mathlib.GroupTheory.GroupAction.FixedPoints

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

English

If a monoid M acts on α, then every element of α is fixed by the identity of M.

Русский

Если моноид M действует на α, то каждый элемент α зафиксирован единицей M.

LaTeX

$$$fixedBy\;\alpha\ (1) = \operatorname{Set.univ}$$$

Lean4

@[to_additive (attr := simp)]
theorem fixedBy_one_eq_univ : fixedBy α (1 : M) = Set.univ :=
  Set.eq_univ_iff_forall.mpr <| one_smul M

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

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

Разделы

Аффилиация

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