Mathlib Changelog
v4
Changelog
About
Github
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.intrinsicStar
View 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.intrinsicStar
View on Github →