Mathlib Map

Theorems · Definition · linear algebra

Holor.assocLeft

{α : Type} → {ds₁ ds₂ ds₃ : List ℕ} → Holor α (ds₁ ++ (ds₂ ++ ds₃)) → Holor α (ds₁ ++ ds₂ ++ ds₃)

Left associator for Holor

Defined in
Mathlib.Data.Holor
Cited by
1 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Holor.mul_assoc0 · cited by 1Holor.mul_assoc0Holor · cited by 24HolorHolor.assocLeftCITED BYCITES

Cites1

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

  • Holorstatement · cited by 24

Cited by1

Results whose statement or proof uses this declaration.