Theorem Algebra.mem_ideal_map_adjoin

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Polynomial/Ideal.lean
feat(Algebra): prerequisites for #31919 (#32118) …
Modified Algebra.mem_ideal_map_adjoinView on Github →
2025-04-08 21:08
Mathlib/RingTheory/Polynomial/Ideal.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified Algebra.mem_ideal_map_adjoinView on Github →
2024-12-02 11:22
Mathlib/RingTheory/Polynomial/Basic.lean
chore(Algebra/Polynomial): don't import `Ideal` when defining `Polynomial.roots` (#19376) …
Modified Algebra.mem_ideal_map_adjoinView on Github →
2024-11-14 17:15
Mathlib/RingTheory/Polynomial/Basic.lean
feat(RingTheory): valuation subrings are maximal local subrings (#19012) …
Added Algebra.mem_ideal_map_adjoinView on Github →