Theorem Algebra.adjoin_mem_exists_aeval

Modification history

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 →