not_isField

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#Int.not_isField

← MathLib Explorer

English

The ring of integers Z is not a field.

Русский

Кольцо целых чисел Z не является полем.

LaTeX

$$$$ \\neg \\mathrm{IsField}(\\mathbb{Z}) $$$$

Lean4

/-- `ℤ` with its usual ring structure is not a field. -/
theorem not_isField : ¬IsField ℤ := fun h =>
  Int.not_even_one <| (h.mul_inv_cancel two_ne_zero).imp fun a => by rw [← two_mul]; exact Eq.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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