toAddValuation_symm_eq — Mathlib

English

The inverse of the canonical equivalence is the forward map, and vice versa; the two maps are mutually inverse.

Русский

Обратное канонического эквивалентного отображения есть прямое отображение, и наоборот; два отображения взаимно обратны.

LaTeX

$$$ toAddValuation^{-1} = toAddValuation. $$ toAddValuation = (toAddValuation)^{-1}. $$$

Lean4

@[simp]
theorem toAddValuation_symm_eq : toAddValuation.symm = ofAddValuation (R := R) (Γ₀ := Γ₀) :=
  rfl

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