not_dvd_unit

Mathlib.Algebra.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Irreducible.not_dvd_unit

English

If p is irreducible, p does not divide a unit.

Русский

Если p несводимо, p не делит единицу.

LaTeX

$$¬ p \mid u$$

Lean4

theorem not_dvd_unit [CommMonoid M] {p : M} (u : Mˣ) (hp : Irreducible p) : ¬p ∣ u :=
  hp.not_dvd_isUnit u.isUnit

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

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

Разделы

Аффилиация

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