exists_unique

Mathlib.Algebra.CharP.Defs

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

English

There exists a unique q with ExpChar R q for domain rings.

Русский

Существует единственный q, удовлетворяющий ExpChar R q, для доменных колец.

LaTeX

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

Lean4

theorem exists_unique [Ring R] [IsDomain R] : ∃! q, ExpChar R q :=
  let ⟨q, H⟩ := ExpChar.exists R
  ⟨q, H, fun _ H2 ↦ ExpChar.eq H2 H⟩

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

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

Разделы

Аффилиация

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