Def Module.End.Units.intrinsicStar

Modification history

2026-02-10 22:14
Mathlib/Algebra/Star/LinearMap.lean
refactor: add type synonym for convolutive product of linear maps and intrinsic star (#34945) …
Deleted Module.End.Units.intrinsicStarView on Github →
2025-11-25 17:10
Mathlib/Algebra/Star/LinearMap.lean
feat(LinearAlgebra/Eigenspace): `mem_eigenspace_intrinsicStar_iff` and `spectrum_intrinsicStar` (#31688)
Added Module.End.Units.intrinsicStarView on Github →