Heather Macbeth
Heather Macbeth
I'd propose making this more lightweight by getting rid of the definition `partial_span` and just stating the lemma `partial_span_dense` in terms of `⨆ J : finset ι, span 𝕜 (J.image...
Yael, I think all these review requests were auto-generated. Maria, let me know if you would like me to look at your PR now, or not yet.
Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do it explicitly....
> > Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do...
If I understand correctly, the mathematical point here is to establish the formula `orthogonal_projection (V i) x` for the `i`-th component of (the symm of) the direct sum decomposition. Perhaps...
I won't have time to work on porting for the next couple of months, sorry; please consider `copy_doc_string` abandoned.
Eric, thank you for your work on this experiment. I'm still not in favour of this approach. I think it would be very off-putting to potential users of the complex...
Note: an alternative solution would be to rename `has_star` to `has_conj`, `star_ring` to `conj_ring`, etc etc! Possibly with localized notation `star` for `conj` in the `cstar_algebra` locale. Did we discuss...
> If we do go down this route though, I think I would prefer to get rid of `conj` entirely and just have `star`. I think having multiple versions of...