Commit 2026-03-17 18:33 1c7e4918

View on Github →

feat(Analysis/CStarAlgebra/Unitary): left multiplication by a unitary as a linear isometric equivalence (#36319)

Estimated changes

Modified Mathlib.lean

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

added def Units.mulLeftLinearEquiv

added theorem Units.mulLeftLinearEquiv_apply

added theorem Units.mulLeftLinearEquiv_mul_apply

added theorem Units.mulLeftLinearEquiv_trans_mulLeftLinearEquiv

added def Units.mulRightLinearEquiv

added theorem Units.mulRightLinearEquiv_apply

added theorem Units.mulRightLinearEquiv_mul_apply

added theorem Units.mulRightLinearEquiv_trans_mulRightLinearEquiv

added theorem Units.symm_mulLeftLinearEquiv

added theorem Units.symm_mulLeftLinearEquiv_apply

added theorem Units.symm_mulRightLinearEquiv

added theorem Units.symm_mulRightLinearEquiv_apply

added theorem Units.toEquiv_mulLeftLinearEquiv

added theorem Units.toEquiv_mulRightLinearEquiv

added theorem Units.toLinearMap_mulLeftLinearEquiv

added theorem Units.toLinearMap_mulRightLinearEquiv

Created Mathlib/Analysis/CStarAlgebra/Unitary/Maps.lean

added theorem Unitary.mulLeft_apply

added theorem Unitary.mulLeft_mul_apply

added theorem Unitary.mulLeft_trans_mulLeft

added theorem Unitary.mulRight_apply

added theorem Unitary.mulRight_mul_apply

added theorem Unitary.mulRight_one

added theorem Unitary.mulRight_trans_mulRight

added theorem Unitary.symm_mulLeft

added theorem Unitary.symm_mulLeft_apply

added theorem Unitary.symm_mulRight

added theorem Unitary.symm_mulRight_apply

added theorem Unitary.toLinearEquiv_mulLeft

added theorem Unitary.toLinearEquiv_mulRight

added theorem Unitary.toLinearMap_mulRight