Commit 2023-07-18 11:09 f287c039

View on Github →

feat: port Order.Irreducible (#5976)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Irreducible.lean

added theorem InfIrred.finset_inf_eq

added theorem InfIrred.ne_top

added def InfIrred

added theorem InfPrime.finset_inf_le

added theorem InfPrime.inf_le

added theorem InfPrime.ne_top

added def InfPrime

added theorem IsMax.not_infIrred

added theorem IsMax.not_infPrime

added theorem IsMin.not_supIrred

added theorem IsMin.not_supPrime

added theorem SupIrred.finset_sup_eq

added theorem SupIrred.ne_bot

added theorem SupIrred.not_isMin

added def SupIrred

added theorem SupPrime.le_finset_sup

added theorem SupPrime.le_sup

added theorem SupPrime.ne_bot

added theorem SupPrime.not_isMin

added def SupPrime

added theorem exists_infIrred_decomposition

added theorem exists_supIrred_decomposition

added theorem infIrred_iff_not_isMax

added theorem infIrred_ofDual

added theorem infIrred_toDual

added theorem infPrime_iff_infIrred

added theorem infPrime_iff_not_isMax

added theorem infPrime_ofDual

added theorem infPrime_toDual

added theorem not_infIrred

added theorem not_infIrred_top

added theorem not_infPrime

added theorem not_infPrime_top

added theorem not_supIrred

added theorem not_supIrred_bot

added theorem not_supPrime

added theorem not_supPrime_bot

added theorem supIrred_iff_not_isMin

added theorem supIrred_ofDual

added theorem supIrred_toDual

added theorem supPrime_iff_not_isMin

added theorem supPrime_iff_supIrred

added theorem supPrime_ofDual

added theorem supPrime_toDual