Commit 2025-06-17 12:53 80a0eb2c

View on Github →

chore: refactor Submodule.baseChange (#26019)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/Lie/BaseChange.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added def LinearEquiv.baseChange

added def LinearMap.baseChange

added def LinearMap.baseChangeHom

added theorem LinearMap.baseChange_add

added theorem LinearMap.baseChange_comp

added theorem LinearMap.baseChange_eq_ltensor

added theorem LinearMap.baseChange_id

added theorem LinearMap.baseChange_mul

added theorem LinearMap.baseChange_neg

added theorem LinearMap.baseChange_one

added theorem LinearMap.baseChange_pow

added theorem LinearMap.baseChange_smul

added theorem LinearMap.baseChange_sub

added theorem LinearMap.baseChange_tmul

added theorem LinearMap.baseChange_zero

added def Module.End.baseChangeHom

modified theorem Submodule.baseChange_bot

added theorem Submodule.baseChange_eq_span

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

deleted def LinearEquiv.baseChange

deleted def LinearMap.baseChange

deleted def LinearMap.baseChangeHom

deleted theorem LinearMap.baseChange_add

deleted theorem LinearMap.baseChange_comp

deleted theorem LinearMap.baseChange_eq_ltensor

deleted theorem LinearMap.baseChange_id

deleted theorem LinearMap.baseChange_mul

deleted theorem LinearMap.baseChange_neg

deleted theorem LinearMap.baseChange_one

deleted theorem LinearMap.baseChange_pow

deleted theorem LinearMap.baseChange_smul

deleted theorem LinearMap.baseChange_sub

deleted theorem LinearMap.baseChange_tmul

deleted theorem LinearMap.baseChange_zero

deleted def Module.End.baseChangeHom

Modified Mathlib/RingTheory/TensorProduct/Free.lean