Theorem Ring.not_isField_of_ne_of_ne

Modification history

2025-12-31 20:48
Mathlib/RingTheory/Ideal/Basic.lean
refactor(RingTheory/Ideal/Basic): clean up proofs (#33418) …
Added Ring.not_isField_of_ne_of_neView on Github →