Theorem Module.End.isUnit_intrinsicStar_iff

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) …
Modified Module.End.isUnit_intrinsicStar_iffView 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.isUnit_intrinsicStar_iffView on Github →