valuation_equiv_symm

Mathlib.Topology.Algebra.Valued.WithVal

URI: https://scilib.ai/kg/mathlib#WithVal.valuation_equiv_symm

English

For any x, the valuation applied after transporting along the inverse equivalence equals the original valuation on x.

Русский

Для любого x выполнение в отношении обратного эквивалента возвращает исходную оценку.

LaTeX

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

Lean4

@[simp]
theorem valuation_equiv_symm (x : R) : valuation v ((equiv v).symm x) = v x :=
  rfl

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

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

Разделы

Аффилиация

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