Commit 2023-05-20 10:23 6de3b498

View on Github →

feat: port Topology.Algebra.Module.Star (#4135)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Module/Star.lean

added def StarModule.decomposeProdAdjointL

added theorem continuous_decomposeProdAdjoint

added theorem continuous_decomposeProdAdjoint_symm

added theorem continuous_selfAdjointPart

added theorem continuous_skewAdjointPart

added def selfAdjointPartL

added def skewAdjointPartL

added def starL