Theorem Algebra.mem_ideal_map_adjoin

Modification history

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 →