mathlib3
dcc45b42 - feat(order/prime_ideal, order/boolean_algebra): small lemmas about prime ideals (#8980)

Commit
4 years ago
feat(order/prime_ideal, order/boolean_algebra): small lemmas about prime ideals (#8980) - Added is_prime.mem_or_compl_mem - Added is_prime.mem_compl_of_not_mem - Added sup_inf_inf_compl
Author
Parents
Loading