adicAbv_coe_le_one

Mathlib.RingTheory.DedekindDomain.AdicValuation

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

← MathLib Explorer

English

For any r ∈ R, the adicAbv of its algebra map into K is ≤ 1.

Русский

Для любого r ∈ R | adicAbv (algebraMap R K r) ≤ 1.

LaTeX

$$v.adicAbv hb (algebraMap R K r) ≤ 1$$

Lean4

theorem adicAbv_coe_le_one {b : NNReal} (hb : 1 < b) (r : R) : v.adicAbv hb (algebraMap R K r) ≤ 1 := by
  simpa [adicAbv, adicAbvDef, toNNReal_le_one_iff hb] using valuation_le_one v r

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

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

Разделы

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

Аффилиация

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