toValuation_ofValuation

Mathlib.RingTheory.Valuation.Basic

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

English

Starting with an AddValuation v, applying the inverse then the forward map gives back v.

Русский

Пусть есть AddValuation v; применение обратного и далее прямого отображения возвращает v.

LaTeX

$$$ toAddValuation (ofAddValuation v) = v. $$$

Lean4

@[simp]
theorem toValuation_ofValuation (v : AddValuation R (Additive Γ₀)ᵒᵈ) : toAddValuation (ofAddValuation v) = v :=
  rfl

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

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

Разделы

Аффилиация

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