valuation_le_one

Mathlib.RingTheory.DedekindDomain.AdicValuation

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.valuation_le_one

← MathLib Explorer

English

For every r ∈ R, the valuation is ≤ 1: v.valuation r ≤ 1.

Русский

Для каждого r ∈ R вектор оценки не превышает 1: v.valuation r ≤ 1.

LaTeX

$$v.valuation(r) \le 1$$

Lean4

/-- The `v`-adic valuation on `R` is bounded above by 1. -/
theorem valuation_le_one (r : R) : v.valuation K r ≤ 1 := by rw [valuation_of_algebraMap]; exact v.intValuation_le_one r

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

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

Разделы

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

Аффилиация

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