symm — Mathlib

English

For semilinear equivalences, applying the symmetry e.symm to x yields the same as applying the inverse to x.

Русский

Для семилинейных эквивалентностей применение симметрии e.symm к x даёт то же, что применение обратного к x.

LaTeX

$$symm_apply {R S : Type*} ... (e : M ≃ₛₗ[σ] M₂) : M₂ → M$$

Lean4

/-- Linear equivalences are symmetric. -/
@[symm]
def symm (e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M :=
  { e.toLinearMap.inverse e.invFun e.left_inv e.right_inv,
    e.toEquiv.symm with
    toFun := e.toLinearMap.inverse e.invFun e.left_inv e.right_inv
    invFun := e.toEquiv.symm.invFun
    map_smul' r x := by rw [map_smulₛₗ] }

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