OAI/Combinatorics/SumProduct/Alignment/WordPlan03.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RationalLattice.exists_physical_face_lift line 50
2. structure OAI.ConstructedWordPlan.GlobalWordPlan.PhysicalMarginalFaceData line 99
3. theorem OAI.ConstructedWordPlan.GlobalWordPlan.own_lifts_from_physical_faces line 150
4. theorem OAI.AllLevelFactorization.Factorization.physical_pivot_mixture_mass line 224