of_dvd_omega0 — Mathlib

English

If (e.oadd n a).NF holds and ω divides repr (e.oadd n a), then repr e ≠ 0 and ω divides repr a.

Русский

Если (e.oadd n a).NF и ω делит repr (e.oadd n a), то repr e ≠ 0 и ω делит repr a.

LaTeX

$$$\forall e:\ ONote,\; \forall n:\ PNat,\; \forall a:\ ONote,\; (e.oadd n a).NF \rightarrow ω \mid (e.oadd n a).repr \rightarrow (repr\; e \neq 0) \wedge ω \mid (repr\; a)$$$

Lean4

theorem of_dvd_omega0 {e n a} (h : NF (ONote.oadd e n a)) : ω ∣ repr (ONote.oadd e n a) → repr e ≠ 0 ∧ ω ∣ repr a := by
  (rw [← opow_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega0_opow)

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