dvd_iff_emultiplicity_pos

Mathlib.RingTheory.Multiplicity

URI: https://scilib.ai/kg/mathlib#dvd_iff_emultiplicity_pos

English

For any a,b in a monoid, 0 < emultiplicity a b iff a divides b.

Русский

Пусть a,b в моноиде; 0 < эмплюситивность a b тогда и только тогда, когда a делит b.

LaTeX

$$$0 < \operatorname{emultiplicity}(a,b) \iff a \mid b$$$

Lean4

theorem dvd_iff_emultiplicity_pos {a b : α} : 0 < emultiplicity a b ↔ a ∣ b :=
  emultiplicity_pos_iff.trans dvd_iff_multiplicity_pos

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

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

Разделы

Аффилиация

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