Commit 2023-06-14 02:21 c7c6b57a

View on Github →

feat: finish forward port of #18877 (#5011) leanprover-community/mathlib#18877

Estimated changes

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

added theorem ContinuousLinearMap.comp_fst_add_comp_snd

added theorem ContinuousLinearMap.coprod_inl_inr

Modified Mathlib/Topology/Basic.lean

Modified test/Continuity.lean