Commit 2024-01-06 13:21 63e722e8

View on Github →

feat(Algebra): generalize Basis.smul (#9382) Add various LinearMap.CompatibleSMul instances that ultimately lead to generalization of Basis.smul to allow a noncommutative base ring. The key observations that allows the generalization are IsScalarTower.smulHomClass and isScalarTower_of_injective.

Estimated changes

Modified Mathlib/Algebra/Algebra/Tower.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem LinearMap.isLinearMap_of_compatibleSMul

added theorem LinearMap.isScalarTower_of_injective

modified theorem LinearMap.map_smul_of_tower

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

added def IsScalarTower.smulHomClass

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

added theorem Basis.isScalarTower_finsupp

added theorem Basis.isScalarTower_of_nonempty

Modified Mathlib/RingTheory/Kaehler.lean