English
If M and N are IsReflexive over R, then M × N is IsReflexive over R.
Русский
Если M и N рефлексивны над R, то их произведение M × N рефлексивно над R.
LaTeX
$$IsReflexive R M × N$$
Lean4
instance _root_.Prod.instModuleIsReflexive [IsReflexive R N] : IsReflexive R (M × N) where
bijective_dual_eval' :=
by
let e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
(dualProdDualEquivDual R M N).dualMap.trans (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
have : Dual.eval R (M × N) = e.symm.comp ((Dual.eval R M).prodMap (Dual.eval R N)) := by ext m f <;> simp [e]
simp only [this, coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
exact (bijective_dual_eval R M).prodMap (bijective_dual_eval R N)
