Commit 2023-06-03 12:15 e28cc527

View on Github →

feat: port Analysis.NormedSpace.TrivSqZeroExt (#4626)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean

added theorem TrivSqZeroExt.eq_smul_exp_of_invertible

added theorem TrivSqZeroExt.eq_smul_exp_of_ne_zero

added theorem TrivSqZeroExt.exp_def

added theorem TrivSqZeroExt.exp_def_of_smul_comm

added theorem TrivSqZeroExt.exp_inl

added theorem TrivSqZeroExt.exp_inr

added theorem TrivSqZeroExt.fst_exp

added theorem TrivSqZeroExt.hasSum_expSeries_of_smul_comm

added theorem TrivSqZeroExt.hasSum_fst_expSeries

added theorem TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm

added theorem TrivSqZeroExt.snd_exp