Jireh Loreaux comments

Results 24 comments of


                                            Jireh Loreaux

trafficstars

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra

I actually considered that a week ago. Actually to be more precise, I sent Yaël a direct message in which I put a (local instance) star structure on the product...

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra

bors merge

feat(analysis/normed_space/category/CStarAlg): categories of C⋆-algebras

Closed to wait for Lean 4. This isn't urgent and probably needs to be implemented slightly differently anyway (to take a `star_ordered_ring` field).

feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms

no need to include me in the copyright.

feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms

bors merge

feat: golf SpectrumRestricts.closedEmbedding_starAlgHom using uniform trickery

Thanks! bors merge

feat: functoriality of ContinuousMap in uniform spaces

Thanks! bors merge

feat(MeasureTheory): generalize `ae` to `OuterMeasureClass`

@urkud wasn't there a Zulip thread about this? Can you link to that please in the PR description?

feat: `mul_le_mul` and `smul_le_smul` variant

ugh, `gcongr` fails to make progress on the first and leaves a side goal for the second. The first is that `smul_le_smul` is not marked `@[gcongr]`, and the second is...

refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices

That's such a small change, and only in a single file, that it's not a big deal. It could even be noise.