coe_symm_toLinearEquiv — Mathlib

English

The coercion of the inverse coalgebra equivalence to a linear equivalence equals the inverse linear equivalence's coercion; i.e., the symmetry respects the linear structure.

Русский

Приведение обратной коалгебраической эквивалентности к линейной эквивалентности совпадает с приведением самой обратной линейной эквивалентности; т.е. симметрия сохраняет линейную структуру.

LaTeX

$$$\\uparrow\\!e^{\\mathrm{symm}} = (e^{})^{\\mathrm{symm}}$$$

Lean4

theorem coe_symm_toLinearEquiv (e : A ≃ₗc[R] B) : ⇑(e : A ≃ₗ[R] B).symm = e.symm :=
  rfl

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