card_support_eq_zero

Mathlib.GroupTheory.Perm.Support

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

English

For a permutation f, f has empty support if and only if f is the identity.

Русский

Перестановка имеет пустую опору тогда и только тогда, когда она тождественна.

LaTeX

$$$\#f.\operatorname{support} = 0 \iff f = 1$$$

Lean4

theorem card_support_eq_zero {f : Perm α} : #f.support = 0 ↔ f = 1 := by rw [Finset.card_eq_zero, support_eq_empty_iff]

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

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

Разделы

Аффилиация

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