Commit f97799f
authored
chore: remove abbreviations linted in mathlib (#764)
C.f.
#522 (comment)1 parent 99a5705 commit f97799f
1 file changed
+0
-3
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
343 | 343 | | |
344 | 344 | | |
345 | 345 | | |
346 | | - | |
347 | 346 | | |
348 | 347 | | |
349 | 348 | | |
| |||
1026 | 1025 | | |
1027 | 1026 | | |
1028 | 1027 | | |
1029 | | - | |
1030 | 1028 | | |
1031 | 1029 | | |
1032 | 1030 | | |
| |||
1385 | 1383 | | |
1386 | 1384 | | |
1387 | 1385 | | |
1388 | | - | |
1389 | 1386 | | |
1390 | 1387 | | |
1391 | 1388 | | |
| |||
0 commit comments