OAI/RepresentationTheory/RestrictedTilting/NormFree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.freeNormRepresentative line 13
2. lemma OAI.FiberFunctorProof.freeNormRepresentative_apply line 20
3. lemma OAI.FiberFunctorProof.free_action_apply line 24
4. lemma OAI.FiberFunctorProof.free_norm_apply line 37
5. lemma OAI.FiberFunctorProof.free_normRepresentative_invariant line 42
6. lemma OAI.FiberFunctorProof.free_normRepresentative_coinvariant line 56
7. theorem OAI.FiberFunctorProof.free_norm_bijective line 83