map_inv

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.map_inv

English

Valuation preserves inversion: v(x^{-1}) = v(x)^{-1}.

Русский

Оценка сохраняет инверсию: v(x^{-1}) = v(x)^{-1}.

LaTeX

$$$ v(x^{-1}) = (v(x))^{-1} $$$

Lean4

theorem map_inv {R : Type*} [DivisionRing R] (v : Valuation R Γ₀) : ∀ x, v x⁻¹ = (v x)⁻¹ :=
  map_inv₀ _

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

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

Разделы

Аффилиация

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