Commit 2025-06-07 11:09 b5368c7d

View on Github →

fix(HahnSeries): solve SMul diamonds (#25408) ... by populating the nsmul and zsmul fields using the existing SMul instances (which must be moved earlier). This also improves the defeq of sub.

Estimated changes

modified theorem HahnSeries.coeff_add'
modified theorem HahnSeries.coeff_neg'
modified theorem HahnSeries.coeff_nsmul
added theorem HahnSeries.coeff_smul'
modified theorem HahnSeries.coeff_sub'
modified theorem HahnSeries.coeff_sub
added theorem HahnSeries.coeff_zero'