Theorem TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm

Modification history

2024-01-08 19:08
Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean
feat(Analysis/NormedSpace/TrivSqZeroExt): generalize to topological spaces (#9491) …
Modified TrivSqZeroExt.hasSum_snd_expSeries_of_smul_commView on Github →
2023-06-03 12:15
Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean
feat: port Analysis.NormedSpace.TrivSqZeroExt (#4626)
Added TrivSqZeroExt.hasSum_snd_expSeries_of_smul_commView on Github →