OAI/Analysis/Cotype/RankFactors.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.exists_rank_pairing_factorsline 12 - theorem
OAI.Cotype.exists_rank_pairing_matrixline 26 - theorem
OAI.Cotype.rank_pairing_contractline 35