Theorem Units.mulRightLinearEquiv_trans_mulRightLinearEquiv

Modification history

2026-03-17 18:33
Mathlib/Algebra/Module/Equiv/Basic.lean
feat(Analysis/CStarAlgebra/Unitary): left multiplication by a unitary as a linear isometric equivalence (#36319)
Added Units.mulRightLinearEquiv_trans_mulRightLinearEquivView on Github →