opLinearEquiv — Mathlib

English

The map sending a vector to its opposite in the opposite module is a linear equivalence.

Русский

Отображение, отправляющее вектор в противоположный в противоположном модуле, является линейным эквивалентом.

LaTeX

$$opLinearEquiv : M ≃ₗ[R] Mᵐᵒᵖ$$

Lean4

/-- The function `op` is a linear equivalence. -/
def opLinearEquiv : M ≃ₗ[R] Mᵐᵒᵖ :=
  { opAddEquiv with map_smul' := MulOpposite.op_smul }

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