Commit 2026-10-27 09:52 37a7c309

View on Github →

feat(LinearAlgebra/TensorProduct/Tower): add baseChange_le_iff_le_comap (#45181) This PR adds a criterion for p.baseChange A ≤ q in terms of submodules instead of sets.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

modified theorem Submodule.baseChange_bot

added theorem Submodule.baseChange_gc

added theorem Submodule.baseChange_iSup

added theorem Submodule.baseChange_le_iff_le_comap

modified theorem Submodule.baseChange_mono

added theorem Submodule.baseChange_sSup

added theorem Submodule.baseChange_sup