coe_coe_symm_apply_coe_apply — Mathlib

English

The symmetry of a given equivalence corresponds to the symmetry of the underlying equivalence as an Equiv.

Русский

Симметрия данной эквивалентности соответствует симметрии базовой эквивалентности как эквив.

LaTeX

$$$ (e: A_1 \simeq_{R} A_2).symm = e^{-1} $$$

Lean4

@[simp]
theorem coe_coe_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₁) :
    (f : A₁ ≃ₐ[R] A₂).symm (f x) = x :=
  EquivLike.left_inv f x

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