OAI/RingTheory/Multiplicity/DuttaData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Lech.IsShortComplex line 14

   Also declared: ComparatorChallenges/DuttaDomain.lean:34 (same declaration text).

2. structure OAI.Lech.IsFiniteHomologyComplex line 23
3. lemma OAI.Lech.IsShortComplex.finiteHomology line 30
4. def OAI.Lech.frobeniusComplex line 36

   Also declared: ComparatorChallenges/DuttaDomain.lean:43 (same declaration text).

5. def OAI.Lech.shortEuler line 41

   Also declared: ComparatorChallenges/DuttaDomain.lean:48 (same declaration text).

6. def OAI.Lech.duttaSequence line 45

   Also declared: ComparatorChallenges/DuttaDomain.lean:52 (same declaration text).

7. def OAI.Lech.duttaMultiplicity line 49

   Also declared: ComparatorChallenges/DuttaDomain.lean:56 (same declaration text).

8. def OAI.Lech.DuttaDomainClaim line 55

   Also declared: ComparatorChallenges/DuttaDomain.lean:62 (same declaration text).