Commit 2023-12-26 21:38 4ad935a4

View on Github →

feat(LinearAlgebra, Cardinal): new cardinal lemmas to generalize some results about Module.rank in #9151 (#9253)

  • Proves that Sup (ciSup) commutes with cardinal addition (ciSup_add_ciSup) and multiplication. Generalize results in Cardinal/Basic introduced in #8842 to achieve this.
  • Use ciSup_add_ciSup to prove that the rank of a module is always at least the rank of a submodule plus the rank of the quotient by the submodule. Deduce that the rank of a product module is at least the sum of the ranks of the two factors.
  • Show that quotienting by a torsion submodule preserves the rank.
  • Golf rank_zero_iff_forall_zero using a recently added lemma.

Estimated changes