Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complete_lattice.coatomic_of_top_compact

Modification history

2021-02-11 06:02
src/order/compactly_generated.lean
perf(ring_theory/{noetherian,ideal/basic}): Simplify proofs of Krull's theorem and related theorems (#6082) …
Added complete_lattice.coatomic_of_top_compactView on Github →