le_valuation_add

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.le_valuation_add

← MathLib Explorer

English

For PadicInt p, if x + y ≠ 0, then min(x.valuation, y.valuation) ≤ (x + y).valuation.

Русский

Для PadicInt p, если x + y ≠ 0, то min(v(x), v(y)) ≤ v(x + y).

LaTeX

$$min(x.valuation, y.valuation) ≤ (x + y).valuation$$

Lean4

theorem le_valuation_add (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation := by zify;
  simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy

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

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

Разделы

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

Аффилиация

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