ncard_smul_set

Mathlib.Algebra.Group.Pointwise.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.ncard_smul_set

English

For a group G acting on α and a ∈ G, the ncard of a • s equals the ncard of s.

Русский

Для группы G, действующей на α, ncard(a • s) = ncard(s).

LaTeX

$$$$ (a \\cdot s).ncard = s.ncard $$$$

Lean4

@[to_additive (attr := simp)]
theorem ncard_smul_set (a : G) (s : Set α) : (a • s).ncard = s.ncard := by simp [ncard]

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

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

Разделы

Аффилиация

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