symm_toLinearEquiv — Mathlib

English

The symmetric coalgebra equivalence e.symm equals the inverse linear equivalence of e, i.e., e.symm = (e : A ≃ₗ[R] B).symm.

Русский

Симметрическая коалгебраическая эквивалентность e.symm равна обратной линейной эквивалентности e: e.symm = (e : A ≃ₗ[R] B).symm.

LaTeX

$$$e.symm = (e : A \\simeq_{\\ell} B).symm$$$

Lean4

@[simp]
theorem symm_toLinearEquiv (e : A ≃ₗc[R] B) : e.symm = (e : A ≃ₗ[R] B).symm :=
  rfl

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