Theorem Isometry.postcomp_pi

Modification history

2026-06-24 17:51
Mathlib/Topology/MetricSpace/Isometry.lean
feat(CStarAlgebra): `IsometricCFC` instance for square `RCLike` matrices (#40272) …
Added Isometry.postcomp_piView on Github →