Commit 2025-04-03 08:58 36198c19
View on Github →chore(RingTheory/PowerSeries/Evaluation): adjust docstrings and names (#23607) This is a minor modification of a very recent file to provide a better support for dot notation.
chore(RingTheory/PowerSeries/Evaluation): adjust docstrings and names (#23607) This is a minor modification of a very recent file to provide a better support for dot notation.