Mathlib Map

Theorems · Definition · several complex variables

FormalMultilinearSeries.compPartialSumSource

ℕ → ℕ → ℕ → Finset ((n : ℕ) × (Fin n → ℕ))

Source set in the change of variables to compute the composition of partial sums of formal power series. See also comp_partialSum.

Defined in
Mathlib.Analysis.Analytic.Composition
Cited by
8 results in Mathlib
Foundations
Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FormalMultilinearSeries.compChangeOfVariables · cited by 7FormalMultilinearSeries.c…FormalMultilinearSeries.compChangeOfVariables_length · cited by 4FormalMultilinearSeries.c…FormalMultilinearSeries.compChangeOfVariables_blocksFun · cited by 3FormalMultilinearSeries.c…FormalMultilinearSeries.compChangeOfVariables_sum · cited by 2FormalMultilinearSeries.c…FormalMultilinearSeries.comp_partialSum · cited by 2FormalMultilinearSeries.c…FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource · cited by 1FormalMultilinearSeries.c…FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 · cited by 1FormalMultilinearSeries.r…FormalMultilinearSeries.mem_compPartialSumSource_iff · cited by 1FormalMultilinearSeries.m…FormalMultilinearSeries.compChangeOfVariables.congr_simp · cited by 0compChangeOfVariables.con…Finset · cited by 13712FinsetFinset.Ico · cited by 450Finset.IcoFintype.piFinset · cited by 86Fintype.piFinsetFinset.sigma · cited by 69Finset.sigmaFormalMultilinearSeries.compP…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by9

Results whose statement or proof uses this declaration.