mathlib3
refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring
#14350
Open
Overview
Commits
45
Changes
View On GitHub

refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring #14350

eric-wieser wants to merge 45 commits into master from eric-wieser/clifford_algebra-semiring-redo
eric-wieser
eric-wieser wip
5e93a5ef
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/quadrat…
601295fb
eric-wieser wip
8252d723
eric-wieser generalize to semiring
e4f78016
eric-wieser fix
31b542e5
eric-wieser fix
25b160a4
eric-wieser remove dead code
7739371f
eric-wieser another one
72785b83
eric-wieser even more
875db5dd
eric-wieser last one (untested)
7ca05693
eric-wieser now build it again
ee443b55
eric-wieser more
cbe02428
eric-wieser Update dual.lean
e908660e
eric-wieser Merge remote-tracking branch 'origin/eric-wieser/bilin_form-tweak' in…
33303c9c
eric-wieser fix build
b10fb6a7
eric-wieser feat(linear_algebra/quadratic_form/isometry): extract from `linear_al…
f9239ec0
eric-wieser fix import
314def35
eric-wieser fix
5a47f58b
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/bilin_f…
d9168e4e
eric-wieser Merge branch 'eric-wieser/bilin_form-tweak' into eric-wieser/quadrati…
9d9f802b
eric-wieser docstrings
17566693
eric-wieser Merge remote-tracking branch 'origin/eric-wieser/split-isometry' into…
55dee123
eric-wieser chore(linear_algebra/quadratic_form/basic): Reorder lemmas
ec8e4230
eric-wieser Merge branch 'eric-wieser/quadratic_form-move-fun_like' into eric-wie…
03c26b81
eric-wieser Merge remote-tracking branch 'origin/master'
19ddebcc
eric-wieser Merge branch into eric-wieser/quadratic_form-semiring
70cc2cb3
eric-wieser reorder
67be7ac0
eric-wieser fix the build
83c69ca4
eric-wieser Merge branch 'eric-wieser/quadratic_form-semiring' of https://github.…
ca118404
eric-wieser fix
3e2e3acc
eric-wieser refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring
6c763140
eric-wieser eric-wieser added WIP
ghost ghost added blocked-by-other-PR
eric-wieser Merge branch 'master' into eric-wieser/quadratic_form-semiring
e615604c
eric-wieser sorry-free
a5df70ba
eric-wieser Merge remote-tracking branch 'origin/staging' into eric-wieser/quadra…
abf2f4a9
eric-wieser add polar_bilin
d4e45c4f
eric-wieser Merge remote-tracking branch 'origin/staging' into eric-wieser/quadra…
abf4b48b
eric-wieser golf
7d1c233e
eric-wieser whitespace
ed9c6267
ghost ghost removed blocked-by-other-PR
ghost
eric-wieser Merge remote-tracking branch 'origin/master' into HEAD
5c7efbda
eric-wieser Merge commit 'HEAD@{1}' into eric-wieser/clifford_algebra-semiring-redo
4cc6c703
eric-wieser Update basic.lean
c6fe6037
eric-wieser fix
9f6eacd1
eric-wieser remove irreducible
8278a09c
eric-wieser Remove redundant line
17f42d66
eric-wieser eric-wieser added maybe-later
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/cliffor…
b166836e
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
WIP maybe-later too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum