Theorem PrimitiveSpectrum.hull_kernel_of_isClosed

Modification history

2025-09-19 07:04
Mathlib/Topology/Order/HullKernel.lean
chore(*): drop some `Decidable`/`Fintype` assumptions (#29785) …
Modified PrimitiveSpectrum.hull_kernel_of_isClosedView on Github →
2025-07-18 08:35
Mathlib/Topology/Order/HullKernel.lean
feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology (#26336) …
Added PrimitiveSpectrum.hull_kernel_of_isClosedView on Github →