@[implicit_reducible]

noncomputable instance TensorCategories.instPivotalCategoryFGModuleCat (k : Type u) [Field k] : PivotalCategory (FGModuleCat k)

FGModuleCat k has a pivotal category structure given by the canonical double-dual evaluation isomorphism together with the tensor-coherence iso of Section 1.38.