mulOpposite — Mathlib

English

The opposite basis b.mulOpposite is the basis of the opposite module Hᵐᵒᵖ obtained by applying the opposite to each basis vector.

Русский

Противоположный базис b.mulOpposite образует базис модуля$H^{\mathrm{op}}$, полученный применением противоположного к каждому вектору базиса.

LaTeX

$$b.mulOpposite is a basis of H^{\mathrm{op}}$$

Lean4

/-- The multiplicative opposite of a basis: `b.mulOpposite i ↦ op (b i)`. -/
noncomputable def mulOpposite (b : Basis ι R H) : Basis ι R Hᵐᵒᵖ :=
  b.map (opLinearEquiv R)

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