Theorem Algebra.adjoin_mem_exists_aeval

Modification history

2026-03-27 10:38
Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean
feat(Subalgebra/Lattice): add notation for Algebra.adjoin (#35928) …
Modified Algebra.adjoin_mem_exists_aevalView on Github →
2026-03-01 10:55
Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean
chore(RingTheory/Adjoin/Polynomial): move to `Basic.lean` (#35883) …
Modified Algebra.adjoin_mem_exists_aevalView on Github →
2025-08-06 17:32
Mathlib/RingTheory/Adjoin/Polynomial.lean
feat(Algebra/Adjoin): singleton as aeval (#27828) …
Added Algebra.adjoin_mem_exists_aevalView on Github →