Commit 2024-10-30 08:00 abfa430b

View on Github →

chore(RingTheory/Ideal): split Quotient.lean into Defs and Basic (#18393) This PR renames and splits files involved in the ideal quotient. Changes:

  • RingTheory/Ideal/Quotient.lean is split into
    • RingTheory/Ideal/Quotient/Defs.lean (definition of ideal quotient and ring structure)
  • RingTheory/Ideal/Quotient/Basic.lean (further results)
  • RingTheory/QuotientNilpotent.lean is renamed to RingTheory/Ideal/Quotient/Nilpotent.lean
  • RingTheory/QuotientNoetherian.lean is renamed to Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean
  • RingTheory/Ideal/QuotientOperations.lean is renamed to Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Estimated changes

deleted theorem Ideal.Quotient.factor_mk
deleted def Ideal.Quotient.lift
deleted theorem Ideal.Quotient.lift_mk
deleted def Ideal.Quotient.mk
deleted theorem Ideal.Quotient.mk_eq_mk
deleted def Ideal.quotEquivOfEq
deleted theorem Ideal.quotEquivOfEq_mk
deleted theorem Ideal.quotEquivOfEq_symm
added theorem Ideal.Quotient.lift_mk
added theorem Ideal.quotEquivOfEq_mk