not_isField

Mathlib.RingTheory.DiscreteValuationRing.Basic

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

← MathLib Explorer

English

A discrete valuation ring is not a field (another statement of the same fact).

Русский

Дискретное величинное кольцо не является полем.

LaTeX

$$$\forall (R : Type) [\mathrm{CommRing R}] [IsDomain R] [IsDiscreteValuationRing R], \lnot \mathrm{IsField} R$$$

Lean4

/-- A discrete valuation ring `R` is not a field. -/
theorem not_isField : ¬IsField R :=
  IsLocalRing.isField_iff_maximalIdeal_eq.not.mpr (not_a_field R)

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

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

Разделы

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

Аффилиация

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