Theorem CharP.ker_intAlgebraMap_eq_span

Modification history

2025-11-02 21:27
Mathlib/Algebra/CharP/Quotient.lean
feat: characteristic of the quotient ring lies in the ideal (#31195) …
Modified CharP.ker_intAlgebraMap_eq_spanView on Github →
2025-04-11 13:00
Mathlib/Algebra/CharP/Quotient.lean
feat(RingTheory/Polynomial/Eisenstein/Generalized): a generalized version of the Eisenstein criterion (#23710) …
Added CharP.ker_intAlgebraMap_eq_spanView on Github →