OAI/Analysis/CharacterCriterion/OrderZeroPair.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted line 31
2. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted_coeff line 36
3. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted_single line 43
4. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted_kronecker line 51
5. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted_left line 71
6. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.weighted_right line 75
7. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.actionLeft line 79
8. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.actionRight line 82
9. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_x_matrices line 85
10. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.right_x_matrices line 92
11. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.linear_field_left line 99
12. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.linear_field_right line 118
13. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_star line 147
14. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_product line 151
15. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_add line 155
16. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_sub line 159
17. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_neg line 163
18. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.interior_matrices_zero line 167
19. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_linear_commute_h line 171
20. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_right_linear_commute line 177
21. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.left_product line 184
22. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.right_product line 191
23. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.cross_product line 199
24. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.cross_product_rev line 203
25. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.field_left line 207
26. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.field_right line 211
27. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.field_left_rev line 215
28. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.field_right_rev line 227
29. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.liftLinear line 240
30. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.lift_apply line 244
31. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.lift_mul line 248
32. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.lift_one line 256
33. lemma OAI.KirchbergRordam.GenericRW.OrderZero.Pair.lift_star line 260
34. def OAI.KirchbergRordam.GenericRW.OrderZero.Pair.dimensionDropHom line 268
35. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.mul_eq_zero_of_total line 285
36. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.commute_of_total_commutator line 291
37. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.commute_of_spokes line 309
38. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwAlpha_diagonal line 340
39. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwAlpha_corner line 345
40. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_commute_corner line 352
41. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_commute_row line 361
42. lemma OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rw_commute_col line 367
43. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwPair line 373
44. def OAI.KirchbergRordam.GenericRW.OrderZero.WeightedUnits.rwHom line 385