OAI/Computability/DepthThree/AlgebraFiniteFibers.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.AlgebraFiniteFibers.fiberEquivKernel line 17
2. theorem OAI.DepthThreeLowerBound.AlgebraFiniteFibers.card_fiber_eq line 36
3. theorem OAI.DepthThreeLowerBound.AlgebraFiniteFibers.card_filter_fiber_eq line 49
4. theorem OAI.DepthThreeLowerBound.AlgebraFiniteFibers.card_eq_mul_card_kernel line 54
5. theorem OAI.DepthThreeLowerBound.AlgebraFiniteFibers.sum_comp line 64
6. theorem OAI.DepthThreeLowerBound.AlgebraFiniteFibers.finiteAvg_comp line 78