The following actions uses node12 which is deprecated and will be forced to run on node16: actions/setup-python@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:45:0: declaration 'ida'.rvector_mul' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/hol_light.lean:65:0: declaration 'hol.wedge.assoc' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:59:0: declaration 'ida'.multivector.ring' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/from_mathlib/basic.lean:34:0: declaration '[anonymous]' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida_derived.lean:60:0: declaration 'ida'.multivector.algebra' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:82:0: declaration 'ida.multivector.has_mul' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:89:0: declaration 'ida.multivector.ring' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/ida.lean:91:0: declaration 'ida.multivector.algebra' uses sorry

/home/runner/work/lean-ga/lean-ga/src/for_mathlib/linear_algebra/tensor_product/inner_product_space.lean:3:0: imported file '/home/runner/work/lean-ga/lean-ga/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean' uses sorry

/home/runner/work/lean-ga/lean-ga/src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean:41:0: declaration 'quadratic_form.pos_def.tmul' uses sorry

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/nursery/chisolm.lean:163:0: 2 + ↑v : multivector 1

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:192:0: 0

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/nursery/chisolm.lean:164:0: 2 + ↑v : multivector 2

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:193:0: [1•e0, 1•e1, 1•e2]

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:194:0: [1•e01, 1•e12, 1•e02]

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:195:0: [-1•e2, 1•e0, 1•e1]

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:196:0: [1•e012, 1•e012]

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:197:0: [1•e012, 1•e012]

/home/runner/work/lean-ga/lean-ga/src/geometric_algebra/translations/laurents.lean:198:0: [0, 0]