Theorem AlgHomClass.instStarAlgHomClass

Modification history

2024-09-09 21:54
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
refactor: deprecate `StarAlgHomClass` and similar as they just duplicate `StarHomClass` (#16591) …
Deleted AlgHomClass.instStarAlgHomClassView on Github →
2024-02-05 18:00
Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Added AlgHomClass.instStarAlgHomClassView on Github →