card_smul_le

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

The size of the smul product is at most the product of the sizes: #(s • t) ≤ #s · #t.

Русский

Размер произведения smul не превосходит произведения размеров: #(s • t) ≤ #s · #t.

LaTeX

$$$ \#(s \cdot t) \le \#s \cdot \#t $$$

Lean4

@[to_additive]
theorem card_smul_le : #(s • t) ≤ #s * #t :=
  card_image₂_le ..

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

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

Разделы

Аффилиация

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