two_le_card_support_of_ne_one

Mathlib.GroupTheory.Perm.Support

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.two_le_card_support_of_ne_one

English

If f ≠ 1, then the size of its support is at least 2.

Русский

Если f ≠ 1, то размер опоры f не меньше 2.

LaTeX

$$$f \neq 1 \Rightarrow 2 \le #f.\operatorname{support}$$$

Lean4

theorem two_le_card_support_of_ne_one {f : Perm α} (h : f ≠ 1) : 2 ≤ #f.support :=
  one_lt_card_support_of_ne_one h

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

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

Разделы

Аффилиация

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