toLinearEquiv_toOpposite — Mathlib

English

The linear isomorphism underlying the opposite construction equals the standard op linear equivalence.

Русский

Линейное изоморфирование, лежащее в основе противоположной конструкции, совпадает с обычным линейным соответствием противоположности.

LaTeX

$$$ toLinearEquiv (toOpposite R A) = opLinearEquiv R $$$

Lean4

@[simp]
theorem toLinearEquiv_toOpposite : toLinearEquiv (toOpposite R A) = opLinearEquiv R :=
  rfl

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