Commit 2023-02-18 20:23 26574897

View on Github →

feat: port Order.PrimeIdeal (#2352)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/PrimeIdeal.lean

added theorem Order.Ideal.IsPrime.mem_compl_of_not_mem

added theorem Order.Ideal.IsPrime.mem_or_compl_mem

added theorem Order.Ideal.IsPrime.mem_or_mem

added theorem Order.Ideal.IsPrime.of_mem_or_mem

added def Order.Ideal.IsPrime.toPrimePair

added theorem Order.Ideal.PrimePair.F_isPrime

added theorem Order.Ideal.PrimePair.F_union_I

added theorem Order.Ideal.PrimePair.I_isPrime

added theorem Order.Ideal.PrimePair.I_isProper

added theorem Order.Ideal.PrimePair.I_union_F

added theorem Order.Ideal.PrimePair.compl_F_eq_I

added theorem Order.Ideal.PrimePair.compl_I_eq_F

added structure Order.Ideal.PrimePair

added theorem Order.Ideal.isPrime_iff_mem_or_compl_mem

added theorem Order.Ideal.isPrime_iff_mem_or_mem

added theorem Order.Ideal.isPrime_of_mem_or_compl_mem

added def Order.PFilter.IsPrime.toPrimePair