smul_def

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

The operation smul on Finsets is defined by s • t = image₂ (· • ·) (s, t).

Русский

Операция smul на множествах Finset задаётся как s • t = image₂ (· • ·) (s, t).

LaTeX

$$$ s \cdot t = \mathrm{image}_2 (\,\cdot \,\, \cdot)(s,t) $$$

Lean4

@[to_additive]
theorem smul_def : s • t = (s ×ˢ t).image fun p : α × β => p.1 • p.2 :=
  rfl

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

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

Разделы

Аффилиация

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