ofValuation_symm_eq — Mathlib

English

The inverse of the AddValuation.ofValuation equivalence is exactly toValuation; i.e., AddValuation.ofValuation.symm = toValuation.

Русский

Обратная к эквивалентности AddValuation.ofValuation равна toValuation; то есть AddValuation.ofValuation.symm = toValuation.

LaTeX

$$$$ \operatorname{ofValuation}^{-1} = \operatorname{toValuation}. $$$$

Lean4

@[simp]
theorem ofValuation_symm_eq : ofValuation.symm = toValuation (R := R) (Γ₀ := Γ₀) :=
  rfl

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