not_char_dvd

Mathlib.Algebra.CharP.Defs

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

English

For CharP R p, if p does not divide n, then n is nonzero in R.

Русский

Для CharP R p, если p не делит n, то n не равен нулю в R.

LaTeX

$$Not (p ∣ n) ⇒ NeZero (n : R)$$

Lean4

theorem not_char_dvd (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero (k : R)] : ¬p ∣ k := by
  rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]

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

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

Разделы

Аффилиация

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