coe_add

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

URI: https://scilib.ai/kg/mathlib#Associates.FactorSet.coe_add

English

The embedding from a sum of factor multisets to a FactorSet preserves addition.

Русский

Встраивание суммы мультисетов факторов в FactorSet сохраняет сложение.

LaTeX

$$$(a + b)^{\uparrow} = a^{\uparrow} + b^{\uparrow}$ in FactorSet.$$

Lean4

theorem coe_add {a b : Multiset { a : Associates α // Irreducible a }} : (↑(a + b) : FactorSet α) = a + b := by
  norm_cast

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

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

Разделы

Аффилиация

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