exists

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ExpChar.exists

English

For any domain ring R, there exists q with ExpChar R q.

Русский

Для любого доменного кольца R существует q such that ExpChar R q.

LaTeX

$$$\\\\exists q \\\\ ExpChar R q$$$

Lean4

theorem «exists» [Ring R] [IsDomain R] : ∃ q, ExpChar R q :=
  by
  obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R
  exacts [⟨1, .zero⟩, ⟨p, .prime hp⟩]

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

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

Разделы

Аффилиация

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