Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsBaseChange.linearMapLeftRightHom_apply
Modification history
2025-11-21 11:20
Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean
feat: base change properties, direct sums, bases, modules of linear maps (#31240) …
Added
IsBaseChange.linearMapLeftRightHom_apply
View on Github →