Theorems · Definition · linear algebra

Module.DualBases.casesOn

{R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {e : ι → M} →
              {ε : ι → Module.Dual R M} →
                {motive : Module.DualBases e ε → Sort u} →
                  (t : Module.DualBases e ε) →
                    ((eval_same : ∀ (i : ι), (ε i) (e i) = 1) →
                        (eval_of_ne : Pairwise fun i j => (ε i) (e j) = 0) →
                          (total : ∀ {m₁ m₂ : M}, (∀ (i : ι), (ε i) m₁ = (ε i) m₂) → m₁ = m₂) →
                            (finite : ∀ (m : M), {i | (ε i) m ≠ 0}.Finite) → motive ⋯) →
                      motive t

Defined in

Mathlib.LinearAlgebra.Dual.Basis

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModule