ofValuation_toValuation

Mathlib.RingTheory.Valuation.Basic

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

English

For any Valuation V, applying toValuation to the AddValuation of V yields V again: toValuation (ofValuation V) = V.

Русский

Для любой оценки V применение toValuation к AddValuation(V) возвращает V: toValuation (ofValuation V) = V.

LaTeX

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

Lean4

@[simp]
theorem ofValuation_toValuation : ofValuation (toValuation v) = v :=
  rfl

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

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

Разделы

Аффилиация

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