Commit 2023-08-09 08:53 07944c77

View on Github →

chore(HahnSeries): use FunLike (#6462)

Estimated changes

Modified Mathlib/RingTheory/HahnSeries.lean

modified theorem HahnSeries.SummableFamily.coe_injective