OAI/Analysis/FreeWords/GNSRows.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.KKFreeWords.FreePartitions.creation_rowline 23 - theorem
OAI.KKFreeWords.FreePartitions.gns_projectionline 41 - theorem
OAI.KKFreeWords.FreePartitions.gns_projection_orthogonalline 50 - theorem
OAI.KKFreeWords.FreePartitions.gns_projection_sumline 54 - theorem
OAI.KKFreeWords.FreePartitions.preservation_eq_compressline 58