English
If M and M' are free R-modules lying in the same universe, then rank_R(M × M') = lift(rank_R M) + lift(rank_R M').
Русский
Пусть M и M' — свободные R-модули в одном верховном мире. Тогда ранк R(M × M') = lift(ранг R M) + lift(ранг R M').
LaTeX
$$$\operatorname{rank}_R (M \times M') = \operatorname{lift}\bigl(\operatorname{rank}_R M\bigr) + \operatorname{lift}\bigl(\operatorname{rank}_R M'\bigr)$$$
Lean4
/-- If `M` and `M'` are free, then the rank of `M × M'` is
`(Module.rank R M).lift + (Module.rank R M').lift`. -/
@[simp]
theorem rank_prod :
Module.rank R (M × M') = Cardinal.lift.{v'} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M') := by
simpa [rank_eq_card_chooseBasisIndex R M, rank_eq_card_chooseBasisIndex R M', lift_umax] using
((chooseBasis R M).prod (chooseBasis R M')).mk_eq_rank.symm
