Theorem Algebra.adjoin_singleton_induction

Modification history

2026-03-01 10:55
Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean
chore(RingTheory/Adjoin/Polynomial): move to `Basic.lean` (#35883) …
Modified Algebra.adjoin_singleton_inductionView on Github →
2025-08-06 17:32
Mathlib/RingTheory/Adjoin/Polynomial.lean
feat(Algebra/Adjoin): singleton as aeval (#27828) …
Added Algebra.adjoin_singleton_inductionView on Github →