Theorem PowerSeries.IsRestricted.one

Modification history

2025-09-22 13:29

Mathlib/RingTheory/PowerSeries/Restricted.lean

feat: restricted power series form a ring (#26089) …

Added PowerSeries.IsRestricted.one View on Github →