Commit 2023-02-11 08:36 2da4e01c

View on Github →

feat: Port/Topology.Spectral.Hom (#2127) port of topology.spectral.hom Also renames instance in Data.FunLike.Basic

Estimated changes

added theorem IsSpectralMap.comp
added structure IsSpectralMap
added theorem SpectralMap.coe_comp
added theorem SpectralMap.coe_copy
added theorem SpectralMap.coe_id
added def SpectralMap.comp
added theorem SpectralMap.comp_apply
added theorem SpectralMap.comp_assoc
added theorem SpectralMap.comp_id
added theorem SpectralMap.copy_eq
added theorem SpectralMap.ext
added theorem SpectralMap.id_apply
added theorem SpectralMap.id_comp
added structure SpectralMap
added theorem isSpectralMap_id