Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

Closed
wants to merge 73 commits into from

Update src/order/ideal.lean

b91a965
Select commit
Loading
Failed to load commit list.
Closed

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

Update src/order/ideal.lean
b91a965
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs