English
If M and N are free R-modules, then their product M × N is free, with a basis obtained as the product of bases: (Module.Free.chooseBasis R M).prod (Module.Free.chooseBasis R N).
Русский
Если M и N свободные R-модули, то их произведение M × N свободно по базису, получаемому как произведение базисов: (Module.Free.chooseBasis R M).prod (Module.Free.chooseBasis R N).
LaTeX
$$$\text{Module.Free }\; R\; (M \times N) \text{ holds with basis } (\mathrm{Module.Free.chooseBasis}\; R\; M) \mathrm{prod} (\mathrm{Module.Free.chooseBasis}\; R\; N).$$$
Lean4
instance prod [Module.Free R M] [Module.Free R N] : Module.Free R (M × N) :=
.of_basis <| (Module.Free.chooseBasis R M).prod (Module.Free.chooseBasis R N)
