dvd

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ringChar.dvd

English

If (x : R) = 0 for some natural x, then ringChar R divides x.

Русский

Если для некоторого натурального x выполнено (x : R) = 0, то ringChar R делит x.

LaTeX

$$$ringChar R \mid x$$$

Lean4

theorem dvd {x : ℕ} (hx : (x : R) = 0) : ringChar R ∣ x :=
  (spec R x).1 hx

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

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

Разделы

Аффилиация

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