Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 23:14 5775ef75

View on Github →

feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime (#6924)

  • ideal_inter_nonempty: the intersection of any two ideals is nonempty. A preorder with joins and this property satisfies that its ideal poset is a lattice.
  • An ideal is prime iff x \inf y \in I implies x \in I or y \in I.
  • A maximal ideal in a distributive lattice is prime.

Estimated changes

added theorem order.ideal.coe_sup_eq
added theorem order.ideal.mem_coe
modified theorem order.ideal.mem_inf
modified theorem order.ideal.mem_sup
added theorem order.inter_nonempty
added theorem order.pfilter.mem_coe