Commit 2026-10-21 16:48 7f647dda

chore: fix a non-reducible diamond in MvPowerSeries (#44400) The following fails before the PR, succeeds after it:

example : ((MvPowerSeries.instCommRingRestricted
    c).toNonUnitalSemiring : NonUnitalSemiring (MvPowerSeries.Restricted S c)) =
    NonUnitalCommRing.toNonUnitalCommSemiring.toNonUnitalSemiring := by
  with_implicit rfl