Commit 2024-12-23 15:42 848ab059

View on Github →

feat: the product of topological modules is a colimit (#20016) ... non-categorically

Estimated changes

Modified Mathlib/LinearAlgebra/Prod.lean

modified theorem LinearMap.ker_prod_ker_le_ker_coprod

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

Modified Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

deleted theorem ContinuousLinearMap.coe_coprod

added theorem ContinuousLinearMap.comp_coprod

modified theorem ContinuousLinearMap.comp_fst_add_comp_snd

modified def ContinuousLinearMap.coprod

added def ContinuousLinearMap.coprodEquiv

added theorem ContinuousLinearMap.coprod_add

deleted theorem ContinuousLinearMap.coprod_apply

added theorem ContinuousLinearMap.coprod_comp_inl

added theorem ContinuousLinearMap.coprod_comp_inr

modified theorem ContinuousLinearMap.coprod_inl_inr

modified theorem ContinuousLinearMap.ker_coprod_of_disjoint_range

modified theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod

modified theorem ContinuousLinearMap.range_coprod