Def Units.mulLeftLinearEquiv

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.mulLeftLinearEquiv View on Github →