Theorems · Theorem · category theory

FGModuleCat.FGModuleCatCoevaluation_apply_one

∀ (K : Type u) [inst : Field K] (V : FGModuleCat K),
  (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatCoevaluation K V).hom) 1 =
    ∑ i, (Module.Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K ↑V).coord i

Defined in

Mathlib.Algebra.Category.FGModuleCat.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field