Theorems · Definition · several complex variables

FormalMultilinearSeries.changeOriginIndexEquiv

(k : ℕ) × (l : ℕ) × { s // s.card = l } ≃ (n : ℕ) × Finset (Fin n)

An auxiliary equivalence useful in the proofs about FormalMultilinearSeries.changeOriginSeries: the set of triples (k, l, s), where s is a Finset (Fin (k + l)) of cardinality l is equivalent to the set of pairs (n, s), where s is a Finset (Fin n). The forward map sends (k, l, s) to (k + l, s) and the inverse map sends (n, s) to (n - Finset.card s, Finset.card s, s). The actual definition is less readable because of problems with non-definitional equalities.

Defined in

Mathlib.Analysis.Analytic.ChangeOrigin

Cited by

9 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound