coe_smul

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

Coercion to sets preserves smul: ↑(s • t) = (s : Set α) • (t : Set β).

Русский

Приведение к множеству сохраняет smul: ↑(s • t) = (s : Set α) • (t : Set β).

LaTeX

$$$ \uparrow (s \cdot t) = (s : Set\,\alpha) \cdot (t : Set\,\beta) $$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_smul (s : Finset α) (t : Finset β) : ↑(s • t) = (s : Set α) • (t : Set β) :=
  coe_image₂ ..

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

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

Разделы

Аффилиация

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