Commit 2024-02-24 18:05 fd1b0477

View on Github →

feat: Add Module.End.baseChangeHom (#10928) This is a more-bundled version of LinearMap.baseChangeHom

Estimated changes

Modified Mathlib/RingTheory/TensorProduct.lean

modified theorem LinearMap.baseChange_comp

added theorem LinearMap.baseChange_id

added theorem LinearMap.baseChange_mul

added theorem LinearMap.baseChange_one

added theorem LinearMap.baseChange_pow

added def Module.End.baseChangeHom