LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive

theorem LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M], (N ≃ₗ[R] Module.Dual R M) → Module.IsReflexive R N

This theorem states that for any commutative ring `R` and any `R`-modules `M` and `N`, if module `M` is reflexive and `N` is in perfect pairing with `M` (i.e., `N` is linearly equivalent to the dual module of `M`), then `N` is also reflexive. Reflexivity of a module means that there is a module homomorphism from the module to its double dual (the dual of its dual) that behaves like the identity on the module.

More concisely: If `M` is a reflexive `R`-module and `N` is in perfect pairing with `M`, then `N` is a reflexive `R`-module.