OAI/Algebra/DepthFive/ImmPairingReindex.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.sum_four_immPaths_compatible_eq line 11

   Source documentation

   Filtered four-path IMM sums are exactly the compatible internal-label sums.

   theorem sum_four_immPaths_compatible_eq {A : Type*} [AddCommMonoid A] (d : ℕ)
       (side : Fin (d + 1) → Bool)
       (f : List (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) →
         List (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) →
         List (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) →
         List (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) → A) :
       let paths := immPaths (d + 1) (Nat.succ_pos d)
   …

   Mentions: OAI.Problem335.immPaths