Theorem unitary.spectrum.unitary_conjugate'

Modification history

2025-10-29 21:09
Mathlib/Algebra/Star/Unitary.lean
chore: move results from `unitary` namespace to `Unitary` (#30697) …
Deleted unitary.spectrum.unitary_conjugate'View on Github →
2024-06-13 01:47
Mathlib/Algebra/Star/Unitary.lean
feat : added `spectrum.conjugate_units` results to `Algebra.Algebra.Spectrum`, and `spectrum.conjugate_unitary` results to `Algebra.Star.Unitary`. (#13729) …
Added unitary.spectrum.unitary_conjugate'View on Github →