natCard_smul_set

Mathlib.Algebra.Group.Pointwise.Set.Card

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

English

For a group G acting on α and a ∈ G, Nat.card ↥(a • s) = Nat.card s.

Русский

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

LaTeX

$$$$ \\mathrm{Nat.card}\\, \\bigl(a \\cdot s\\bigr) = \\mathrm{Nat.card}\\, s $$$$

Lean4

@[to_additive]
theorem natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s := by simp

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

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

Разделы

Аффилиация

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