compChangeOfVariables_length — Mathlib

English

The length of the resulting composition after applying compChangeOfVariables equals the input length i.1.

Русский

Длина результирующего композиционного блока после применения compChangeOfVariables равна входной длине i.1.

LaTeX

$$$\\text{Length}(\\mathrm{compChangeOfVariables}\\ m\\ M\\ N\\ i\\ hi)\\;\\text{snd}.length = i.1$$$

Lean4

@[simp]
theorem compChangeOfVariables_length (m M N : ℕ) {i : Σ n, Fin n → ℕ} (hi : i ∈ compPartialSumSource m M N) :
    Composition.length (compChangeOfVariables m M N i hi).2 = i.1 :=
  by
  rcases i with ⟨k, blocks_fun⟩
  dsimp [compChangeOfVariables]
  simp only [Composition.length, length_ofFn]

Похожие утверждения