Theorem Ideal.natCast_mem_of_charP_quotient

Modification history

2025-11-02 21:27
Mathlib/Algebra/CharP/Quotient.lean
feat: characteristic of the quotient ring lies in the ideal (#31195) …
Added Ideal.natCast_mem_of_charP_quotientView on Github →