Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-24 03:45 f414fcaa

View on Github →

feat(analysis/analytic/composition): filling small holes in existing API (#5822) This PR expands the existing API around the composition of formal multilinear series. Also makes the finset argument to finset.prod_subtype and finset.add_subtype explicit instead of implicit.

Estimated changes

Modified src/analysis/analytic/composition.lean

added def continuous_multilinear_map.comp_along_composition

added theorem continuous_multilinear_map.comp_along_composition_apply

added def continuous_multilinear_map.comp_along_composition_aux

added theorem continuous_multilinear_map.comp_along_composition_aux_bound

added theorem formal_multilinear_series.apply_composition_single

deleted def formal_multilinear_series.comp_along_composition_multilinear

deleted theorem formal_multilinear_series.comp_along_composition_multilinear_bound

added theorem formal_multilinear_series.comp_coeff_one

added theorem formal_multilinear_series.comp_continuous_linear_map_apply_composition

added theorem formal_multilinear_series.comp_remove_zero

modified theorem formal_multilinear_series.id_comp

added theorem formal_multilinear_series.remove_zero_apply_composition

added theorem formal_multilinear_series.remove_zero_comp_of_pos

Modified src/analysis/calculus/formal_multilinear_series.lean

added def formal_multilinear_series.comp_continuous_linear_map

added theorem formal_multilinear_series.comp_continuous_linear_map_apply

added def formal_multilinear_series.remove_zero

added theorem formal_multilinear_series.remove_zero_coeff_succ

added theorem formal_multilinear_series.remove_zero_coeff_zero

added theorem formal_multilinear_series.remove_zero_of_pos

Modified src/combinatorics/composition.lean

modified def composition.blocks_fun

added theorem composition.blocks_fun_mem_blocks

added theorem composition.eq_ones_iff_le_length

added theorem composition.eq_ones_iff_length

deleted theorem composition.eq_single_iff

added theorem composition.eq_single_iff_length

added theorem composition.ne_single_iff

added theorem composition.one_le_blocks_fun

Modified src/data/fintype/basic.lean

added theorem fintype.card_eq_one_of_forall_eq

Modified src/data/fintype/card.lean

added theorem finset.prod_to_finset_eq_subtype

Modified src/ring_theory/integral_domain.lean