Theorem MvPowerSeries.C_surjective

Modification history

2026-04-13 12:24

Mathlib/RingTheory/MvPowerSeries/Basic.lean

feat(MvPowerSeries): MvPowerSeries.C is injective and add `@[grind inj]` (#37689)

Added MvPowerSeries.C_surjective View on Github →