Commit 2024-10-29 15:17 90ab0257

View on Github →

chore(RingTheory/Ideal): split up Ideal/Basic.lean (#18383) This PR splits off various definitions and results from RingTheory/Ideal/Basic.lean:

  • Ideal goes to Ideal/Defs.lean
  • results on ⊥, ⊤, ⊔, ⊓ go to Ideal/Lattice.lean
  • Ideal.IsPrime goes to Ideal/Prime.lean
  • IsPrincipalIdealDomain and Ideal.span go to Ideal/Span.lean
  • Ideal.IsMaximal goes to Ideal/Maximal.lean

Estimated changes

deleted theorem Ideal.IsMaximal.eq_of_le
deleted theorem Ideal.IsMaximal.isPrime
deleted theorem Ideal.IsMaximal.ne_top
deleted theorem Ideal.IsPrime.mem_or_mem
deleted theorem Ideal.IsPrime.ne_top
deleted theorem Ideal.bot_isMaximal
deleted theorem Ideal.bot_prime
deleted theorem Ideal.eq_bot_of_prime
deleted theorem Ideal.eq_bot_or_top
deleted theorem Ideal.eq_top_iff_one
deleted theorem Ideal.eq_top_of_unit_mem
deleted theorem Ideal.exists_le_maximal
deleted theorem Ideal.exists_maximal
deleted theorem Ideal.ext
deleted theorem Ideal.factors_decreasing
deleted theorem Ideal.isMaximal_def
deleted theorem Ideal.isMaximal_iff
deleted theorem Ideal.isPrime_iff
deleted theorem Ideal.mem_bot
deleted theorem Ideal.mem_iInf
deleted theorem Ideal.mem_iSup_of_mem
deleted theorem Ideal.mem_inf
deleted theorem Ideal.mem_of_dvd
deleted theorem Ideal.mem_sInf
deleted theorem Ideal.mem_sSup_of_mem
deleted theorem Ideal.mem_span
deleted theorem Ideal.mem_span_insert'
deleted theorem Ideal.mem_span_insert
deleted theorem Ideal.mem_span_pair
deleted theorem Ideal.mem_span_singleton'
deleted theorem Ideal.mem_span_singleton
deleted theorem Ideal.mem_sup_left
deleted theorem Ideal.mem_sup_right
deleted theorem Ideal.mul_mem_left
deleted theorem Ideal.mul_mem_right
deleted theorem Ideal.mul_sub_mul_mem
deleted theorem Ideal.ne_top_iff_one
deleted theorem Ideal.not_isPrime_iff
deleted def Ideal.ofRel
deleted theorem Ideal.pow_mem_of_mem
deleted theorem Ideal.pow_mem_of_pow_mem
deleted def Ideal.span
deleted theorem Ideal.span_empty
deleted theorem Ideal.span_eq
deleted theorem Ideal.span_eq_bot
deleted theorem Ideal.span_iUnion
deleted theorem Ideal.span_insert
deleted theorem Ideal.span_le
deleted theorem Ideal.span_mono
deleted theorem Ideal.span_one
deleted theorem Ideal.span_pair_comm
deleted theorem Ideal.span_singleton_neg
deleted theorem Ideal.span_singleton_one
deleted theorem Ideal.span_union
deleted theorem Ideal.span_univ
deleted theorem Ideal.span_zero
deleted theorem Ideal.submodule_span_eq
deleted theorem Ideal.subset_span
deleted theorem Ideal.sum_mem
added theorem Ideal.ext
added theorem Ideal.mem_of_dvd
added theorem Ideal.mul_mem_left
added theorem Ideal.mul_mem_right
added theorem Ideal.mul_sub_mul_mem
added theorem Ideal.pow_mem_of_mem
added theorem Ideal.sum_mem
added theorem Ideal.eq_bot_or_top
added theorem Ideal.eq_top_iff_one
added theorem Ideal.mem_bot
added theorem Ideal.mem_iInf
added theorem Ideal.mem_iSup_of_mem
added theorem Ideal.mem_inf
added theorem Ideal.mem_sInf
added theorem Ideal.mem_sSup_of_mem
added theorem Ideal.mem_sup_left
added theorem Ideal.mem_sup_right
added theorem Ideal.ne_top_iff_one
added theorem Ideal.IsMaximal.ne_top
added theorem Ideal.bot_isMaximal
added theorem Ideal.exists_maximal
added theorem Ideal.isMaximal_def
added theorem Ideal.isMaximal_iff
added theorem Ideal.IsPrime.ne_top
added theorem Ideal.bot_prime
added theorem Ideal.eq_bot_of_prime
added theorem Ideal.isPrime_iff
added theorem Ideal.not_isPrime_iff
added theorem Ideal.mem_span
added theorem Ideal.mem_span_insert'
added theorem Ideal.mem_span_insert
added theorem Ideal.mem_span_pair
added def Ideal.ofRel
added def Ideal.span
added theorem Ideal.span_empty
added theorem Ideal.span_eq
added theorem Ideal.span_eq_bot
added theorem Ideal.span_iUnion
added theorem Ideal.span_insert
added theorem Ideal.span_le
added theorem Ideal.span_mono
added theorem Ideal.span_one
added theorem Ideal.span_pair_comm
added theorem Ideal.span_union
added theorem Ideal.span_univ
added theorem Ideal.span_zero
added theorem Ideal.subset_span