Theorem Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin

Modification history

2026-03-18 16:39
Mathlib/RingTheory/Adjoin/Polynomial/Bivariate.lean
feat(Adjoin/Polynomial/Bivariate): IsAlgebraic.adjoin_singleton (#35874) …
Added Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoinView on Github →