Theorems · Inductive type · linear algebra

Module.DualBases

{R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (ι → M) → (ι → Module.Dual R M) → Prop

e and ε have characteristic properties of a basis and its dual

Defined in

Mathlib.LinearAlgebra.Dual.Basis

Cited by

15 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModule