∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M],
  ⟦SemimoduleCat.of R (Module.Finite.reprₛ R M)⟧ * ⟦SemimoduleCat.of R (Module.Dual R (Module.Finite.reprₛ R M))⟧ = 1