Commit 2023-03-06 15:29 cf97ef3d

View on Github →

feat: port Algebra.Star.Module (#2441)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Star/Module.lean

added def StarModule.decomposeProdAdjoint

added theorem StarModule.selfAdjointPart_add_skewAdjointPart

added theorem algebraMap_star_comm

added def selfAdjoint.submodule

added def selfAdjointPart

added def skewAdjoint.submodule

added def skewAdjointPart

added def starLinearEquiv

added theorem star_int_cast_smul

added theorem star_inv_int_cast_smul

added theorem star_inv_nat_cast_smul

added theorem star_nat_cast_smul

added theorem star_rat_cast_smul

added theorem star_rat_smul