WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Formal power series

Revision #3150 → #3231 · back to history

modifiedProduct topology on R^N598ee06d4cb7
FieldFrom #3150To #3231
mathlib.declPowerSeries.WithPiTopologyPowerSeries.WithPiTopology.instTopologicalSpace