Def LaurentSeries.powerSeriesAlgEquiv

Modification history

2026-03-05 14:15

Mathlib/RingTheory/LaurentSeries.lean

feat(RatFunc): add notation for RatFunc (#36172) …

Modified LaurentSeries.powerSeriesAlgEquiv View on Github →

2025-01-27 10:06

Mathlib/RingTheory/LaurentSeries.lean

feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) …

Added LaurentSeries.powerSeriesAlgEquiv View on Github →