OAI/RepresentationTheory/UniversalSquare/Band/CommonPath.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Common Path.

  1. def OAI.Saxl.Band.extendFourBasis line 14
  2. lemma OAI.Saxl.Band.extendFourBasis_pathBasis line 17
  3. theorem OAI.Saxl.Band.odd_path_common_basis line 27