OAI/RepresentationTheory/RestrictedTilting/RelativeTrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.relativeTrace line 13
2. lemma OAI.FiberFunctorProof.relativeTrace_apply line 16
3. def OAI.FiberFunctorProof.relativeTraceHom line 21
4. lemma OAI.FiberFunctorProof.relativeTrace_precomp line 31
5. lemma OAI.FiberFunctorProof.relativeTrace_postcomp line 39