Theorem Unitary.isUnit_coe

Modification history

2025-11-11 22:41

Mathlib/Algebra/Star/Unitary.lean

chore(Analysis/Matrix/Spectrum): change `spectral_theorem` to use `conjStarAlgAut` map (#31322)

Added Unitary.isUnit_coe View on Github →