OAI/Algebra/Drinfeld/RealLie.lean

GitHub source file

296 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RealDeligneDrinfeld.freeLie_induction line 8
2. abbrev OAI.RealDeligneDrinfeld.L line 30
3. def OAI.RealDeligneDrinfeld.x line 31
4. def OAI.RealDeligneDrinfeld.y line 32
5. def OAI.RealDeligneDrinfeld.eval line 34
6. abbrev OAI.RealDeligneDrinfeld.Edge line 37
7. abbrev OAI.RealDeligneDrinfeld.BraidFree line 38
8. def OAI.RealDeligneDrinfeld.chord line 40
9. def OAI.RealDeligneDrinfeld.braidRelations line 44
10. def OAI.RealDeligneDrinfeld.braidIdeal line 51
11. abbrev OAI.RealDeligneDrinfeld.T4 line 54
12. def OAI.RealDeligneDrinfeld.t line 55
13. def OAI.RealDeligneDrinfeld.IsSolution line 57
14. def OAI.RealDeligneDrinfeld.W line 64
15. structure OAI.RealDeligneDrinfeld.Tangent line 97
16. def OAI.RealDeligneDrinfeld.Tangent.equiv line 101
17. instance OAI.RealDeligneDrinfeld.(instance at line 107) line 107
18. instance OAI.RealDeligneDrinfeld.(instance at line 108) line 108
19. instance OAI.RealDeligneDrinfeld.(instance at line 109) line 109
20. theorem OAI.RealDeligneDrinfeld.Tangent.ext line 113
21. theorem OAI.RealDeligneDrinfeld.Tangent.base_zero line 116
22. theorem OAI.RealDeligneDrinfeld.Tangent.velocity_zero line 117
23. theorem OAI.RealDeligneDrinfeld.Tangent.base_add line 118
24. theorem OAI.RealDeligneDrinfeld.Tangent.velocity_add line 119
25. theorem OAI.RealDeligneDrinfeld.Tangent.base_smul line 121
26. theorem OAI.RealDeligneDrinfeld.Tangent.velocity_smul line 122
27. theorem OAI.RealDeligneDrinfeld.Tangent.base_lie line 124
28. theorem OAI.RealDeligneDrinfeld.Tangent.velocity_lie line 125
29. instance OAI.RealDeligneDrinfeld.(instance at line 128) line 128
30. instance OAI.RealDeligneDrinfeld.(instance at line 151) line 151
31. def OAI.RealDeligneDrinfeld.tangentLift line 154
32. def OAI.RealDeligneDrinfeld.D line 157
33. def OAI.RealDeligneDrinfeld.ihara line 159
34. theorem OAI.RealDeligneDrinfeld.eval_x line 161
35. theorem OAI.RealDeligneDrinfeld.eval_y line 163
36. def OAI.RealDeligneDrinfeld.Tangent.baseHom line 166
37. theorem OAI.RealDeligneDrinfeld.tangentLift_base line 172
38. theorem OAI.RealDeligneDrinfeld.D_x line 179
39. theorem OAI.RealDeligneDrinfeld.D_y line 180
40. theorem OAI.RealDeligneDrinfeld.D_zero line 181
41. theorem OAI.RealDeligneDrinfeld.D_add line 182
42. theorem OAI.RealDeligneDrinfeld.D_smul line 183
43. theorem OAI.RealDeligneDrinfeld.D_lie line 184
44. def OAI.RealDeligneDrinfeld.derivation line 187
45. theorem OAI.RealDeligneDrinfeld.derivation_apply line 195
46. theorem OAI.RealDeligneDrinfeld.derivation_ext line 197
47. theorem OAI.RealDeligneDrinfeld.D_zero_left line 208
48. theorem OAI.RealDeligneDrinfeld.D_add_left line 213
49. theorem OAI.RealDeligneDrinfeld.D_smul_left line 218
50. inductive OAI.RealDeligneDrinfeld.WeightedWord line 223
51. def OAI.RealDeligneDrinfeld.weightPiece line 228
52. abbrev OAI.RealDeligneDrinfeld.OddFree line 231
53. def OAI.RealDeligneDrinfeld.oddWeight line 232
54. abbrev OAI.RealDeligneDrinfeld.Fn line 233
55. abbrev OAI.RealDeligneDrinfeld.Ln line 234
56. abbrev OAI.RealDeligneDrinfeld.Wn line 235
57. def OAI.RealDeligneDrinfeld.Graded line 237
58. abbrev OAI.RealDeligneDrinfeld.OddCompletion line 240
59. abbrev OAI.RealDeligneDrinfeld.WCompletion line 241
60. instance OAI.RealDeligneDrinfeld.(instance at line 243) line 243
61. instance OAI.RealDeligneDrinfeld.(instance at line 244) line 244
62. def OAI.RealDeligneDrinfeld.completed line 246
63. def OAI.RealDeligneDrinfeld.completedInv line 249
64. def OAI.RealDeligneDrinfeld.MainStatement line 255
65. abbrev OAI.RealDeligneDrinfeld.AssociativeModel.FL line 269
66. abbrev OAI.RealDeligneDrinfeld.AssociativeModel.A line 270
67. def OAI.RealDeligneDrinfeld.AssociativeModel.atom line 273
68. def OAI.RealDeligneDrinfeld.AssociativeModel.embed line 275
69. theorem OAI.RealDeligneDrinfeld.AssociativeModel.embed_of line 277
70. def OAI.RealDeligneDrinfeld.AssociativeModel.dynkinWord line 280
71. theorem OAI.RealDeligneDrinfeld.AssociativeModel.dynkinWord_cons line 285
72. def OAI.RealDeligneDrinfeld.AssociativeModel.wordLinear line 291
73. theorem OAI.RealDeligneDrinfeld.AssociativeModel.wordLinear_single line 295
74. def OAI.RealDeligneDrinfeld.AssociativeModel.dynkin line 300
75. def OAI.RealDeligneDrinfeld.AssociativeModel.wordAct line 302
76. def OAI.RealDeligneDrinfeld.AssociativeModel.act line 305
77. theorem OAI.RealDeligneDrinfeld.AssociativeModel.act_single line 308
78. theorem OAI.RealDeligneDrinfeld.AssociativeModel.wordAct_of_apply line 311
79. theorem OAI.RealDeligneDrinfeld.AssociativeModel.act_embed line 315
80. theorem OAI.RealDeligneDrinfeld.AssociativeModel.dynkinWord_append line 322
81. def OAI.RealDeligneDrinfeld.AssociativeModel.homogeneous line 330
82. theorem OAI.RealDeligneDrinfeld.AssociativeModel.single_mem_homogeneous line 334
83. theorem OAI.RealDeligneDrinfeld.AssociativeModel.mul_homogeneous line 338
84. theorem OAI.RealDeligneDrinfeld.AssociativeModel.dynkin_mul line 355
85. theorem OAI.RealDeligneDrinfeld.AssociativeModel.dynkin_embed_word line 370
86. def OAI.RealDeligneDrinfeld.AssociativeModel.normalizedDynkin line 394
87. theorem OAI.RealDeligneDrinfeld.AssociativeModel.normalizedDynkin_homogeneous line 397
88. theorem OAI.RealDeligneDrinfeld.AssociativeModel.normalizedDynkin_embed_word line 408
89. theorem OAI.RealDeligneDrinfeld.AssociativeModel.mem_word_span line 414
90. theorem OAI.RealDeligneDrinfeld.AssociativeModel.normalizedDynkin_embed line 438
91. theorem OAI.RealDeligneDrinfeld.AssociativeModel.embed_injective line 448
92. structure OAI.RealDeligneDrinfeld.FreeDerivations.Jet line 458
93. def OAI.RealDeligneDrinfeld.FreeDerivations.Jet.equiv line 462
94. instance OAI.RealDeligneDrinfeld.FreeDerivations.(instance at line 468) line 468
95. instance OAI.RealDeligneDrinfeld.FreeDerivations.(instance at line 469) line 469
96. instance OAI.RealDeligneDrinfeld.FreeDerivations.(instance at line 470) line 470
97. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.ext line 474
98. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.base_zero line 477
99. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.velocity_zero line 478
100. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.base_add line 479
101. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.velocity_add line 480
102. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.base_smul line 482
103. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.velocity_smul line 483
104. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.base_lie line 485
105. theorem OAI.RealDeligneDrinfeld.FreeDerivations.Jet.velocity_lie line 486
106. instance OAI.RealDeligneDrinfeld.FreeDerivations.(instance at line 489) line 489
107. instance OAI.RealDeligneDrinfeld.FreeDerivations.(instance at line 499) line 499
108. def OAI.RealDeligneDrinfeld.FreeDerivations.Jet.baseHom line 502
109. def OAI.RealDeligneDrinfeld.FreeDerivations.jetLift line 511
110. theorem OAI.RealDeligneDrinfeld.FreeDerivations.jetLift_base line 514
111. def OAI.RealDeligneDrinfeld.FreeDerivations.extend line 523
112. theorem OAI.RealDeligneDrinfeld.FreeDerivations.extend_of line 538
113. theorem OAI.RealDeligneDrinfeld.FreeDerivations.ext line 543
114. theorem OAI.RealDeligneDrinfeld.FreeDerivations.extend_unique line 554
115. def OAI.RealDeligneDrinfeld.FreeDerivations.pair line 561
116. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_of_left line 565
117. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_of_right line 569
118. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_of_other line 575
119. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_comm line 579
120. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_self line 588
121. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_disjoint line 595
122. theorem OAI.RealDeligneDrinfeld.FreeDerivations.pair_three line 610
123. def OAI.RealDeligneDrinfeld.BraidRepresentation.fiber line 637
124. def OAI.RealDeligneDrinfeld.BraidRepresentation.base line 638
125. def OAI.RealDeligneDrinfeld.BraidRepresentation.chord line 640
126. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_none_none line 646
127. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_none_some line 647
128. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_some_none line 648
129. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_some_some line 649
130. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_comm line 651
131. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_self line 654
132. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.base_fiber line 657
133. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.fiber_base line 662
134. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_disjoint line 667
135. theorem OAI.RealDeligneDrinfeld.BraidRepresentation.chord_three line 674
136. abbrev OAI.RealDeligneDrinfeld.BraidModel.Fiber line 713
137. abbrev OAI.RealDeligneDrinfeld.BraidModel.Der line 714
138. abbrev OAI.RealDeligneDrinfeld.BraidModel.Model line 715
139. def OAI.RealDeligneDrinfeld.BraidModel.chord line 716
140. theorem OAI.RealDeligneDrinfeld.BraidModel.chord_comm line 719
141. theorem OAI.RealDeligneDrinfeld.BraidModel.chord_self line 722
142. def OAI.RealDeligneDrinfeld.BraidModel.preMap line 725
143. theorem OAI.RealDeligneDrinfeld.BraidModel.preMap_chord line 727
144. theorem OAI.RealDeligneDrinfeld.BraidModel.ideal_le_ker line 736
145. def OAI.RealDeligneDrinfeld.BraidModel.map line 750
146. theorem OAI.RealDeligneDrinfeld.BraidModel.map_t line 758
147. theorem OAI.RealDeligneDrinfeld.AssociativeModel.coeff_rotate line 766
148. theorem OAI.RealDeligneDrinfeld.AssociativeModel.coeff_starts_ne line 777
149. theorem OAI.RealDeligneDrinfeld.AssociativeModel.coeff_contains_ne line 787
150. theorem OAI.RealDeligneDrinfeld.AssociativeModel.coeff_eq_zero_of_letter_ne line 798
151. theorem OAI.RealDeligneDrinfeld.AssociativeModel.dynkinWord_all_eq line 804
152. theorem OAI.RealDeligneDrinfeld.AssociativeModel.centralizer_generator line 820
153. theorem OAI.RealDeligneDrinfeld.map_eval line 844
154. theorem OAI.RealDeligneDrinfeld.eval_self line 853
155. theorem OAI.RealDeligneDrinfeld.eval_commutes line 858
156. theorem OAI.RealDeligneDrinfeld.chord_comm line 868
157. theorem OAI.RealDeligneDrinfeld.t_comm line 872
158. theorem OAI.RealDeligneDrinfeld.t_disjoint line 876
159. theorem OAI.RealDeligneDrinfeld.t_three line 883
160. def OAI.RealDeligneDrinfeld.BraidModel.inclusion line 891
161. theorem OAI.RealDeligneDrinfeld.BraidModel.map_inclusion line 894
162. theorem OAI.RealDeligneDrinfeld.BraidModel.inclusion_injective line 899
163. theorem OAI.RealDeligneDrinfeld.commute_symm line 909
164. theorem OAI.RealDeligneDrinfeld.evals_commute line 912
165. theorem OAI.RealDeligneDrinfeld.eval_add_of_commuting line 920
166. theorem OAI.RealDeligneDrinfeld.eval_vanish_of_commuting line 935
167. theorem OAI.RealDeligneDrinfeld.eval_central_shift line 949
168. def OAI.RealDeligneDrinfeld.T4Universal.pre line 959
169. theorem OAI.RealDeligneDrinfeld.T4Universal.pre_chord line 962
170. def OAI.RealDeligneDrinfeld.T4Universal.lift line 973
171. theorem OAI.RealDeligneDrinfeld.T4Universal.lift_t line 992
172. theorem OAI.RealDeligneDrinfeld.t_self line 997
173. def OAI.RealDeligneDrinfeld.t4Rename line 999
174. theorem OAI.RealDeligneDrinfeld.t4Rename_t line 1008
175. theorem OAI.RealDeligneDrinfeld.solution_swap line 1011
176. theorem OAI.RealDeligneDrinfeld.solution_three line 1018
177. theorem OAI.RealDeligneDrinfeld.free_action_inner line 1024
178. def OAI.RealDeligneDrinfeld.InnerSemiDirect.lift line 1061
179. theorem OAI.RealDeligneDrinfeld.InnerSemiDirect.lift_inl line 1071
180. theorem OAI.RealDeligneDrinfeld.InnerSemiDirect.lift_inr line 1073
181. abbrev OAI.RealDeligneDrinfeld.SpecialFiber.F line 1079
182. def OAI.RealDeligneDrinfeld.SpecialFiber.fa line 1080
183. def OAI.RealDeligneDrinfeld.SpecialFiber.fb line 1081
184. def OAI.RealDeligneDrinfeld.SpecialFiber.fc line 1082
185. def OAI.RealDeligneDrinfeld.SpecialFiber.action line 1084
186. abbrev OAI.RealDeligneDrinfeld.SpecialFiber.M line 1085
187. def OAI.RealDeligneDrinfeld.SpecialFiber.a line 1087
188. def OAI.RealDeligneDrinfeld.SpecialFiber.b line 1088
189. def OAI.RealDeligneDrinfeld.SpecialFiber.c line 1089
190. def OAI.RealDeligneDrinfeld.SpecialFiber.u line 1090
191. def OAI.RealDeligneDrinfeld.SpecialFiber.v line 1091
192. def OAI.RealDeligneDrinfeld.SpecialFiber.w line 1092
193. theorem OAI.RealDeligneDrinfeld.SpecialFiber.au line 1094
194. theorem OAI.RealDeligneDrinfeld.SpecialFiber.bu line 1097
195. theorem OAI.RealDeligneDrinfeld.SpecialFiber.cu line 1100
196. theorem OAI.RealDeligneDrinfeld.SpecialFiber.av line 1103
197. theorem OAI.RealDeligneDrinfeld.SpecialFiber.bv line 1106
198. theorem OAI.RealDeligneDrinfeld.SpecialFiber.cv line 1109
199. def OAI.RealDeligneDrinfeld.SpecialFiber.chord line 1113
200. theorem OAI.RealDeligneDrinfeld.SpecialFiber.chord_symm line 1123
201. theorem OAI.RealDeligneDrinfeld.SpecialFiber.chord_zero line 1126
202. theorem OAI.RealDeligneDrinfeld.SpecialFiber.chord_disjoint line 1128
203. theorem OAI.RealDeligneDrinfeld.SpecialFiber.chord_three line 1139
204. def OAI.RealDeligneDrinfeld.SpecialFiber.representation line 1149
205. theorem OAI.RealDeligneDrinfeld.SpecialFiber.representation_t line 1152
206. def OAI.RealDeligneDrinfeld.SpecialFiber.fiberSpec line 1155
207. def OAI.RealDeligneDrinfeld.SpecialFiber.baseSpec line 1157
208. theorem OAI.RealDeligneDrinfeld.SpecialFiber.fiberSpec_fa line 1159
209. theorem OAI.RealDeligneDrinfeld.SpecialFiber.fiberSpec_fb line 1160
210. theorem OAI.RealDeligneDrinfeld.SpecialFiber.fiberSpec_fc line 1161
211. theorem OAI.RealDeligneDrinfeld.SpecialFiber.baseSpec_x line 1162
212. theorem OAI.RealDeligneDrinfeld.SpecialFiber.baseSpec_y line 1163
213. theorem OAI.RealDeligneDrinfeld.SpecialFiber.spec_equivariant line 1165
214. def OAI.RealDeligneDrinfeld.SpecialFiber.specialize line 1173
215. theorem OAI.RealDeligneDrinfeld.SpecialFiber.specialize_a line 1175
216. theorem OAI.RealDeligneDrinfeld.SpecialFiber.specialize_b line 1176
217. theorem OAI.RealDeligneDrinfeld.SpecialFiber.specialize_c line 1177
218. theorem OAI.RealDeligneDrinfeld.SpecialFiber.specialize_u line 1178
219. theorem OAI.RealDeligneDrinfeld.SpecialFiber.specialize_v line 1179
220. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_right line 1181
221. def OAI.RealDeligneDrinfeld.SpecialFiber.Fa line 1185
222. def OAI.RealDeligneDrinfeld.SpecialFiber.Fb line 1186
223. def OAI.RealDeligneDrinfeld.SpecialFiber.Fc line 1187
224. theorem OAI.RealDeligneDrinfeld.SpecialFiber.Fa_inl line 1189
225. theorem OAI.RealDeligneDrinfeld.SpecialFiber.Fb_inl line 1193
226. theorem OAI.RealDeligneDrinfeld.SpecialFiber.Fc_inl line 1197
227. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_comm_a line 1202
228. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_comm_b line 1206
229. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_comm_c line 1210
230. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_comm_sum line 1214
231. theorem OAI.RealDeligneDrinfeld.SpecialFiber.fiber_identity line 1219
232. theorem OAI.RealDeligneDrinfeld.SpecialFiber.Fb_specialize line 1230
233. theorem OAI.RealDeligneDrinfeld.SpecialFiber.pentagon line 1241
234. theorem OAI.RealDeligneDrinfeld.SpecialFiber.pentagon_reverse line 1247
235. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_bv_shift line 1254
236. theorem OAI.RealDeligneDrinfeld.SpecialFiber.eval_bu_shift line 1264
237. theorem OAI.RealDeligneDrinfeld.SpecialFiber.delta_a line 1274
238. theorem OAI.RealDeligneDrinfeld.SpecialFiber.delta_c line 1284
239. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.base_neg line 1302
240. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.velocity_neg line 1303
241. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.base_sub line 1304
242. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.velocity_sub line 1305
243. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.mk_add line 1307
244. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.mk_neg line 1309
245. theorem OAI.RealDeligneDrinfeld.Differentiation.Jet.mk_sub line 1311
246. theorem OAI.RealDeligneDrinfeld.Differentiation.eval_base line 1314
247. def OAI.RealDeligneDrinfeld.Differentiation.adPower line 1317
248. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_zero line 1322
249. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_succ line 1324
250. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_smul line 1325
251. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_zero_right line 1329
252. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_self line 1332
253. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_zero_left line 1340
254. def OAI.RealDeligneDrinfeld.Differentiation.slope line 1343
255. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_x line 1346
256. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_y line 1347
257. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_zero line 1348
258. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_add line 1349
259. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_smul line 1351
260. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_lie line 1353
261. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_zero_direction line 1357
262. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_add_direction line 1365
263. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_smul_direction line 1374
264. theorem OAI.RealDeligneDrinfeld.Differentiation.word_pos line 1383
265. def OAI.RealDeligneDrinfeld.Differentiation.DiagonalData line 1388
266. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_bracket line 1393
267. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_word line 1441
268. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_homogeneous line 1460
269. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_neg_direction line 1482
270. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_inner line 1486
271. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_swap line 1495
272. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_slope line 1499
273. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_first line 1504
274. def OAI.RealDeligneDrinfeld.Differentiation.G line 1515
275. theorem OAI.RealDeligneDrinfeld.Differentiation.eval_G line 1517
276. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_G line 1521
277. def OAI.RealDeligneDrinfeld.Differentiation.fiberEval line 1537
278. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_fa line 1539
279. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_fb line 1541
280. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_fc line 1543
281. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_spec line 1546
282. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_base line 1554
283. theorem OAI.RealDeligneDrinfeld.Differentiation.fiberEval_Fb line 1562
284. theorem OAI.RealDeligneDrinfeld.Differentiation.transverse line 1567
285. theorem OAI.RealDeligneDrinfeld.Differentiation.slope_G_formula line 1613
286. def OAI.RealDeligneDrinfeld.Differentiation.swapJet line 1623
287. theorem OAI.RealDeligneDrinfeld.Differentiation.mixed_slope line 1632
288. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_base line 1639
289. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_radial line 1643
290. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_transverse_self line 1653
291. theorem OAI.RealDeligneDrinfeld.Differentiation.adPower_zero_base line 1667
292. theorem OAI.RealDeligneDrinfeld.Differentiation.mixed_scalar line 1675
293. theorem OAI.RealDeligneDrinfeld.Differentiation.diagonal_scalar_zero line 1700
294. theorem OAI.RealDeligneDrinfeld.Differentiation.special_linearization line 1719
295. theorem OAI.RealDeligneDrinfeld.Differentiation.special_G_zero line 1727
296. theorem OAI.RealDeligneDrinfeld.Differentiation.special_identity line 1751