Commit 2025-12-31 20:48 957423a1

View on Github →

refactor(RingTheory/Ideal/Basic): clean up proofs (#33418) This PR cleans up RingTheory/Ideal/Basic by introducing some intermediate results isField_iff_maximal_bot, exists_maximal_of_not_isField, not_isField_of_ne_of_ne.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ideal.bot_lt_of_maximal

added theorem Ring.exists_maximal_of_not_isField

added theorem Ring.isField_iff_maximal_bot

added theorem Ring.not_isField_of_ne_of_ne