OAI/NumberTheory/OrdinaryCorrelations/HighTrace/GateAncestor.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.OrdinaryCorrelations.Rerooting.gateAncestorline 22 - lemma
OAI.OrdinaryCorrelations.Rerooting.reversed_left_injectiveline 26 - theorem
OAI.OrdinaryCorrelations.Rerooting.reroot_reverseline 39