dvd_prod

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

URI: https://scilib.ai/kg/mathlib#Multiset.dvd_prod

English

If a ∈ s, then a divides s.prod in a commutative monoid.

Русский

Если a принадлежит s, то a делит s.prod в коммутативном моноиде.

LaTeX

$$$ \text{dvd_prod: } a \in s \Rightarrow a \mid s.prod $$$

Lean4

theorem dvd_prod : a ∈ s → a ∣ s.prod :=
  Quotient.inductionOn s (fun l a h ↦ by simpa using List.dvd_prod h) a

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

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

Разделы

Аффилиация

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