Commit 2025-12-08 14:29 eb93f7a9

View on Github →

chore(RingTheory/Polynomial): make Ideal.isPrime_map_C_of_isPrime an instance (#32472)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Ideal.isPrime_map_C_of_isPrime

Modified Mathlib/RingTheory/Spectrum/Prime/IsOpenComapC.lean