spin_group) : Spin Group
#16040

Open

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group #16040

Biiiilly wants to merge 15 commits into master from spin_group

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group

7ccabf5b

change length

d3368365

Biiiilly added awaiting-review

Biiiilly requested a review from

kbuzzard 3 years ago

Biiiilly requested a review from

eric-wieser 3 years ago

change doc

ae6bbc5f

change length

82b7b60d

eric-wieser commented on 2022-08-15

Biiiilly removed awaiting-review

Biiiilly added awaiting-author

Merge remote-tracking branch 'origin/master' into spin_group

752f1e03

new def of lipschitz

d73690a9

Biiiilly added WIP

mainly change doc

fa6393cb

Biiiilly added blocked-by-other-PR

Biiiilly removed WIP

Biiiilly removed awaiting-author

simplify proof a bit

676fdc5d

Biiiilly added awaiting-review

add missing proof

02978bbf

change inst

6886a9f5

change inst

4331453a

Biiiilly requested a review from

eric-wieser 3 years ago

change doc

4179e43e

mathlib-dependent-issues-bot removed blocked-by-other-PR

Nothing

a9b386d9

Merge branch 'master' into spin_group

9600012f

changes on dependent issues

3e7eb7d2

Biiiilly removed awaiting-review

Biiiilly added WIP

eric-wieser commented on 2022-10-30

kim-em added too-late

Reviewers

utensil

eric-wieser

kbuzzard

Assignees

No one assigned

Labels

WIP too-late

Milestone

No milestone

mathlib3 feat(linear_algebra/clifford_algebra/spin_group) : Spin Group #16040 Open

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group #16040

mathlib3
feat(linear_algebra/clifford_algebra/spin_group) : Spin Group
#16040

Open