OAI/Computability/DepthThree/IrreducibleEncoding.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.DepthThreeLowerBound.BinaryAlgebra.polynomialBitsline 9 - theorem
OAI.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_polynomialBitsline 12 - theorem
OAI.DepthThreeLowerBound.exists_irreducible_inputPolynomialBitsline 30