Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
formal_multilinear_series.change_origin_summable_aux_j_inj
Modification history
2020-06-18 22:26
src/analysis/analytic/basic.lean
chore(*): regularize naming using injective (#3071) …
Deleted
formal_multilinear_series.change_origin_summable_aux_j_inj
View on Github →
2020-04-14 07:18
src/analysis/analytic/basic.lean
chore(analysis): two more -T50000 challenges (#2393) …
Added
formal_multilinear_series.change_origin_summable_aux_j_inj
View on Github →