Commit 2024-06-26 08:17 f0298510

View on Github →

chore: move IsLinearMap theorems to their own file (#14116)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/LinearMap/Prod.lean

added theorem IsLinearMap.isLinearMap_add

added theorem IsLinearMap.isLinearMap_sub

Modified Mathlib/Analysis/Convex/Star.lean

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem IsLinearMap.isLinearMap_add

deleted theorem IsLinearMap.isLinearMap_sub