Commit 2025-06-09 11:40 eb04d3df

View on Github →

fix(HahnSeries): solve SMul Rat diamonds, and lemmas about casts (#25413) This fixes the instances diamonds in the Rat and NNRat actions, and adds lemmas about {Nat,Int,NNRat,NRat}.castand of{Nat,Scientific}. There is no motivation here beyond cleaning up diamonds.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.single_add

added theorem HahnSeries.single_neg

added theorem HahnSeries.single_sub

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.single_zero_intCast

added theorem HahnSeries.single_zero_natCast

added theorem HahnSeries.single_zero_nnratCast

added theorem HahnSeries.single_zero_ofNat

modified theorem HahnSeries.single_zero_one

added theorem HahnSeries.single_zero_ratCast

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.single_zero_ofScientific