OAI/Topology/ArtinGroups/Complexes/NegativeTwistLoweredGenerator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwist_lowered_generator_socle_at_floor line 19
  2. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwist_floor_of_socle_zero line 87