Categorical packaging of the contragredient dual

def QuotientSubmoduleEquidistribution.Contragredient.dualFunctor (K : Type uK) (R : Type uR) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor (FGModuleCat R)ᵒᵖ (FGModuleCat Rᵐᵒᵖ)

The K-linear dual as a contravariant functor from finitely generated R-modules to finitely generated Rᵐᵒᵖ-modules.