Commit 2023-11-25 18:19 632ea778

View on Github →

chore: delete LinearMap.extendScalars which duplicates LinearMap.baseChange (#8617) For consistency, we also rename Submodule.extendScalars to Submodule.baseChange and likewise for LieSubmodule.

Estimated changes

Modified Mathlib/Algebra/Lie/BaseChange.lean

added theorem LieModule.toEndomorphism_baseChange

deleted theorem LieModule.toEndomorphism_extendScalars

added def LieSubmodule.baseChange

added theorem LieSubmodule.baseChange_bot

added theorem LieSubmodule.baseChange_top

added theorem LieSubmodule.coe_baseChange

deleted theorem LieSubmodule.coe_extendScalars

deleted def LieSubmodule.extendScalars

deleted theorem LieSubmodule.extendScalars_bot

deleted theorem LieSubmodule.extendScalars_top

added theorem LieSubmodule.lie_baseChange

deleted theorem LieSubmodule.lie_extendScalars

added theorem LieSubmodule.mem_baseChange_iff

deleted theorem LieSubmodule.mem_extendScalars_iff

added theorem LieSubmodule.tmul_mem_baseChange_of_mem

deleted theorem LieSubmodule.tmul_mem_extendScalars_of_mem

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieSubmodule.lowerCentralSeries_tensor_eq_baseChange

deleted theorem LieSubmodule.lowerCentralSeries_tensor_eq_extendScalars

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

deleted def LinearMap.extendScalars

deleted theorem LinearMap.extendScalars_comp

deleted theorem LinearMap.extendScalars_tmul

added def Submodule.baseChange

added theorem Submodule.baseChange_bot

added theorem Submodule.baseChange_span

added theorem Submodule.baseChange_top

deleted def Submodule.extendScalars

deleted theorem Submodule.extendScalars_bot

deleted theorem Submodule.extendScalars_span

deleted theorem Submodule.extendScalars_top

added theorem Submodule.tmul_mem_baseChange_of_mem

deleted theorem Submodule.tmul_mem_extendScalars_of_mem

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_baseChange

deleted theorem LinearMap.trace_extendScalars

Modified Mathlib/RingTheory/TensorProduct.lean

added theorem LinearMap.baseChange_comp

added theorem LinearMap.toMatrix_baseChange

deleted theorem LinearMap.toMatrix_extendScalars