valuation_le_one

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.valuation_le_one

English

For any a in A, A.valuation(a) ≤ 1.

Русский

Для любого a в A, A.valuation(a) ≤ 1.

LaTeX

$$$A.valuation(a) \le 1$$$

Lean4

theorem valuation_le_one (a : A) : A.valuation a ≤ 1 :=
  (ValuationRing.mem_integer_iff A K _).2 ⟨a, rfl⟩

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

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

Разделы

Аффилиация

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