Commit 2025-11-21 11:20 a5a0f4c5

feat: base change properties, direct sums, bases, modules of linear maps (#31240) Establish various IsBaseChange properties:

• direct sums commute with base change
• when the source module is finite free, modules of linear maps commute with base change (on the right, on both sides, and for endomorphisms).
• a base change of a free module is free, with compatible bases.