Theorems · Theorem · group theory
Fin.insertNth_mul
∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x y : α i)
(p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q- Defined in
- Mathlib.Algebra.Group.Fin.Tuple
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fin.succAbovestatement and proof · cited by 249
- Fin.insertNthstatement · cited by 95
- Fin.insertNth_binopproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.