dvdNotUnit_of_dvd_of_not_dvd — Mathlib

English

If a divides b and b does not divide a, then DvdNotUnit(a,b).

Русский

Если a делится на b и наоборот b не делится на a, то DvdNotUnit(a,b).

LaTeX

$$a \mid b \land \lnot (b \mid a) \Rightarrow \mathrm{DvdNotUnit}(a,b)$$

Lean4

theorem dvdNotUnit_of_dvd_of_not_dvd {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) : DvdNotUnit a b :=
  by
  constructor
  · rintro rfl
    exact hnd (dvd_zero _)
  · rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd

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