Commit 2025-09-04 11:48 173cc8d8

View on Github →

feat(RingTheory): lemmas on finiteness of LinearMap and Module.End (#24015)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/End.lean

modified def LinearMap.compRight

modified theorem LinearMap.compRight_apply

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

modified def LinearMap.lcomp

modified theorem LinearMap.lcomp_apply'

modified theorem LinearMap.lcomp_apply

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem LinearMap.surjective_comp_linearProjOfIsCompl

added theorem LinearMap.surjective_comp_subtype_of_isComplemented

Modified Mathlib/RingTheory/Finiteness/Basic.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

added theorem Module.Finite.of_isComplemented_codomain

added theorem Module.Finite.of_isComplemented_domain