dens_smul_finset

Mathlib.Algebra.Group.Pointwise.Finset.Density

URI: https://scilib.ai/kg/mathlib#Finset.dens_smul_finset

English

Density is invariant under group action on Finset: for any a, dens(a • s) = dens(s).

Русский

Плотность сохраняется при скалярном действии группы на Finset: для любого a, dens(a • s) = dens(s).

LaTeX

$$$\\text{dens}(a \\cdot s) = \\text{dens}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem dens_smul_finset [Fintype β] (a : α) (s : Finset β) : (a • s).dens = s.dens := by simp [dens]

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

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

Разделы

Аффилиация

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