le_or_le

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.Prime.le_or_le

English

Prime (mk p) is equivalent to Prime p for p ∈ M.

Русский

Prime( mk(p) ) эквивалентно Prime(p) для p ∈ M.

LaTeX

$$$ \operatorname{Prime}(\mathrm{mk}(p)) \iff \operatorname{Prime}(p) $$$

Lean4

theorem le_or_le {p : Associates M} (hp : Prime p) {a b : Associates M} (h : p ≤ a * b) : p ≤ a ∨ p ≤ b :=
  hp.2.2 a b h

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

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

Разделы

Аффилиация

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