Def HahnSeries.coeff.addMonoidHom

Modification history

2024-02-16 04:51

Mathlib/RingTheory/HahnSeries.lean

chore: Split HahnSeries file (#10595) …

Modified HahnSeries.coeff.addMonoidHom View on Github →

2023-05-23 12:52

Mathlib/RingTheory/HahnSeries.lean

feat: port RingTheory.HahnSeries (#4261)

Added HahnSeries.coeff.addMonoidHom View on Github →