OAI/NumberTheory/Ostmann/Tree/QuartetFamilyPullback.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Tree.Quartet.pairModeline 11 - theorem
OAI.Ostmann.Tree.Quartet.modeMultiplier_castline 13 - theorem
OAI.Ostmann.Tree.Quartet.pairTest_zero_differenceline 19 - def
OAI.Ostmann.Tree.Quartet.NodeInput.crossFamilyFunctionline 25 - theorem
OAI.Ostmann.Tree.Quartet.NodeInput.crossFamily_pullback_pointline 30