symm_mk — Mathlib

English

If you construct a linear equivalence from data including e and its potential inverse f, the inverse of that constructed equivalence equals e.symm.

Русский

Если построить линейное эквивалентное отображение из данных, включая e и его предполагаемое обратное f, то обратное к построенному эквиваленту равно e.symm.

LaTeX

$$$(\\text{constructed})^{-1} = e^{-1}$$$

Lean4

@[simp]
theorem symm_mk (f h₁ h₂ h₃ h₄) :
    (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm =
      { symm_mk.aux e f h₁ h₂ h₃ h₄ with
        toFun := f
        invFun := e } :=
  rfl

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