Def PrimitiveSpectrum.OrderGenerates

Modification history

2025-07-18 08:35

Mathlib/Topology/Order/HullKernel.lean

feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology (#26336) …

Added PrimitiveSpectrum.OrderGenerates View on Github →