Theorem Unitary.toLinearMap_mulRight

Modification history

2026-05-29 13:23
Mathlib/Analysis/CStarAlgebra/Unitary/Maps.lean
chore: bump toolchain to v4.31.0-rc1 (#39980)
Modified Unitary.toLinearMap_mulRightView on Github →
2026-03-17 18:33
Mathlib/Analysis/CStarAlgebra/Unitary/Maps.lean
feat(Analysis/CStarAlgebra/Unitary): left multiplication by a unitary as a linear isometric equivalence (#36319)
Added Unitary.toLinearMap_mulRightView on Github →