toValuation_ofValuation

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#AddValuation.toValuation_ofValuation

English

The other direction of the equivalence is also true: toValuation (ofValuation v) = v for any additive valuation v.

Русский

Также верно обратное: toValuation (ofValuation v) = v для любой аддитивной оценки v.

LaTeX

$$$$ \mathrm{toValuation}(\mathrm{ofValuation}(v)) = v. $$$$

Lean4

@[simp]
theorem toValuation_ofValuation (v : Valuation R (Multiplicative Γ₀ᵒᵈ)) : toValuation (ofValuation v) = v :=
  rfl

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

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

Разделы

Аффилиация

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