OAI/Combinatorics/Progressions/Nilpotent/DiagramExternalNetMaskedNiltests.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.RationalFilteredNilmanifold.exists_externalNet_masked_niltestsline 17 - theorem
OAI.Erdos3.RationalFilteredNilmanifold.DiagramNativeExternalNetConclusion.exists_masked_niltestsline 101