instIsNontrivial

Mathlib.NumberTheory.Padics.ValuativeRel

URI: https://scilib.ai/kg/mathlib#Padic.instIsNontrivial

English

The p-adic field ℚ_[p] is a nontrivial valued ring.

Русский

Поле p-адических чисел ℚ_[p] является ненулевой (непростой) ценностной областью.

LaTeX

$$$\\text{Padic.instIsNontrivial}$$$

Lean4

instance : IsNontrivial ℚ_[p] where
  condition := ⟨ValuativeRel.valuation _ p, valuation_p_ne_zero _, (valuation_p_lt_one _).ne⟩

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

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

Разделы

Аффилиация

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