OAI/RepresentationTheory/RestrictedTilting/LatticeNumerator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiberFunctorProof.coordinateMap_injective line 11
2. def OAI.FiberFunctorProof.coordinateEquiv line 16
3. lemma OAI.FiberFunctorProof.coordinateEquiv_apply line 20
4. def OAI.FiberFunctorProof.latticeNumerator line 30
5. lemma OAI.FiberFunctorProof.latticeNumerator_coordinates line 35
6. lemma OAI.FiberFunctorProof.latticeDenominator_mem line 44
7. def OAI.FiberFunctorProof.latticeDenominator line 54
8. lemma OAI.FiberFunctorProof.latticeNumerator_denominator line 58
9. lemma OAI.FiberFunctorProof.latticeDenominator_numerator line 66