mulOpposite_repr_eq — Mathlib

English

The representation of the opposite basis equals the composition of opLinearEquiv with the original representation.

Русский

Представление противоположного базиса равно композиции opLinearEquiv и исходного представления.

LaTeX

$$b.mulOpposite.repr = (opLinearEquiv R).symm.trans b.repr$$

Lean4

theorem mulOpposite_repr_eq (b : Basis ι R H) : b.mulOpposite.repr = (opLinearEquiv R).symm.trans b.repr :=
  rfl

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