ofBijective_symm_apply_apply — Mathlib

English

The inverse of an algebra equivalence is its symmetry map: ϕ^{-1} = ϕ.symm.

Русский

Обратное к алгебраическому эквивалентному отображению равно его симметрическому отображению: ϕ^{-1} = ϕ.symm.

LaTeX

$$$ \\varphi^{-1} = \\varphi^{\\mathrm{symm}} $$$

Lean4

@[simp]
theorem ofBijective_symm_apply_apply (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) (x : A₁) :
    (ofBijective f hf).symm (f x) = x :=
  (ofBijective f hf).symm_apply_apply x

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