Theorems · Definition · linear algebra

Module.Basis.mulOpposite

{R : Type u_1} →
  {H : Type u_2} →
    {ι : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid H] → [inst_2 : Module R H] → Module.Basis ι R H → Module.Basis ι R Hᵐᵒᵖ

The multiplicative opposite of a basis: b.mulOpposite i ↦ op (b i).

Defined in

Mathlib.LinearAlgebra.Basis.MulOpposite

Cited by

7 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModule