Theorems · Theorem · combinatorics

Fin.inv_partialProd_mul_eq_contractNth

∀ {n : ℕ} {G : Type u_3} [inst : Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n),
  (Fin.partialProd g (j.succ.succAbove k.castSucc))⁻¹ * Fin.partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 => x1 * x2) g k

Let (g₀, g₁, ..., gₙ) be a tuple of elements in Gⁿ⁺¹. Then if k < j, this says (g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ. If k = j, it says (g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁. If k > j, it says (g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁. Useful for defining group cohomology.

Defined in

Mathlib.Algebra.BigOperators.Fin

Cited by

0 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext

Assumes

Group