Commit 2025-11-25 17:10 4ebe3c7b

View on Github →

feat(LinearAlgebra/Eigenspace): mem_eigenspace_intrinsicStar_iff and spectrum_intrinsicStar (#31688)

Estimated changes

Modified Mathlib/Algebra/Star/LinearMap.lean

added theorem Module.End.IsUnit.intrinsicStar

added def Module.End.Units.intrinsicStar

added theorem Module.End.isUnit_intrinsicStar_iff

added theorem Module.End.mem_eigenspace_intrinsicStar_iff

added theorem Module.End.spectrum_intrinsicStar