PR #18179: feat(linear_algebra/clifford): make clifford_a...

Stream: triage

[Random Issue Bot]

Today I chose PR 18179 for discussion!

feat(linear_algebra/clifford): make clifford_algebra irreducible in a Lean4 compatible way
Created by @None (@sgouezel) on 2023-01-15
Labels: awaiting-review, mathport, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Wait @Johan Commelin I don't think this should be merged yet.

[Yaël Dillies]

Oh I see this was already addressed by Eric.

[Johan Commelin]

whatever