toEquiv_symm — Mathlib

English

The inverse of an affine equivalence corresponds to the inverse equivalence on the underlying vector/torsor structure.

Русский

Обратное к аффинному эквиваленту соответствует обратному эквиваленту на базовой структуре тензора.

LaTeX

$$$e^{-1}_{toEquiv} = (e^{-1})_{toEquiv}$$$

Lean4

@[simp]
theorem toEquiv_symm (e : P₁ ≃ᵃ[k] P₂) : e.symm.toEquiv = e.toEquiv.symm :=
  rfl

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