dvdNotUnit_of_lt

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.dvdNotUnit_of_lt

← MathLib Explorer

English

If a < b in Associates M, then DvdNotUnit a b.

Русский

Если a < b в Associates(M), то DvdNotUnit a b.

LaTeX

$$$ a < b \Rightarrow \mathrm{DvdNotUnit}(a,b) $$$

Lean4

theorem dvdNotUnit_of_lt {a b : Associates M} (hlt : a < b) : DvdNotUnit a b :=
  by
  constructor
  · rintro rfl
    apply not_lt_of_ge _ hlt
    apply dvd_zero
  rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
  refine ⟨x, ?_, rfl⟩
  contrapose! ndvd
  rcases ndvd with ⟨u, rfl⟩
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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