symm_equivOfInverse — Mathlib

English

The symmetric form of the inverse construction for the prime variant gives (equivOfInverse' f1 f2 h1 h2).symm = equivOfInverse' f2 f1 h2 h1.

Русский

Симметрическая форма обратной конструкции для варианта с апострофом: (equivOfInverse' f1 f2 h1 h2).symm = equivOfInverse' f2 f1 h2 h1.

LaTeX

$$$ (equivOfInverse'\\ f_1 f_2 h_1 h_2).symm = equivOfInverse' f_2 f_1 h_2 h_1 $$$

Lean4

@[simp]
theorem symm_equivOfInverse (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ h₁ h₂) :
    (equivOfInverse f₁ f₂ h₁ h₂).symm = equivOfInverse f₂ f₁ h₂ h₁ :=
  rfl

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