Def Polynomial.ofSubring

Modification history

2026-02-09 13:22

Mathlib/RingTheory/Polynomial/Basic.lean

refactor: move `Polynomial.toSubring` to a new file (#34661) …

Deleted Polynomial.ofSubring View on Github →

2023-03-30 13:14

Mathlib/RingTheory/Polynomial/Basic.lean

feat: port RingTheory.Polynomial.Basic (#3067)

Added Polynomial.ofSubring View on Github →