OAI/GroupTheory/PolycyclicRecognition/Geometry/MultilinearBarBoundary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Multilinear evaluation annihilates the abelian bar boundary

Contracting two adjacent entries by addition is the sum of the evaluations with either entry deleted. The alternating boundary sum then telescopes.

  1. theorem OAI.PolycyclicRecognition.multilinear_contractNth_add line 18
  2. theorem OAI.PolycyclicRecognition.alternating_adjacent_sum line 51
  3. theorem OAI.PolycyclicRecognition.contractNth_last_eq line 67
  4. theorem OAI.PolycyclicRecognition.multilinear_abelian_bar_boundary line 73