of_not_dvd

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#NeZero.of_not_dvd

English

If p ∣ n is false, then NeZero (n : R).

Русский

Если не выполняется p ∣ n, то NeZero (n : R).

LaTeX

$$[CharP R p] \land \neg (p \mid n) \Rightarrow NeZero (n : R)$$

Lean4

theorem of_not_dvd [CharP R p] (h : ¬p ∣ n) : NeZero (n : R) :=
  ⟨(CharP.cast_eq_zero_iff R p n).not.mpr h⟩

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

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

Разделы

Аффилиация

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