Commit 2021-03-30 03:44 b449a3cd
View on Github →feat(order/ideal, order/pfilter, order/prime_ideal): added is_ideal
, is_pfilter
, is_prime
, is_maximal
, prime_pair
(#6656)
Proved basic lemmas about them. Also extended the is_proper API.
Made the pfilter
arguments of some lemmas explicit:
pfilter.nonempty
pfilter.directed