Jireh Loreaux comments

Results 24 comments of


                                            Jireh Loreaux

trafficstars

Removing dynamic plugins

Just to throw in my 2 cents: I also compile my plugins into the main gitit binary. My feeling is that in gitit's current state (i.e., many people building from...

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring

@Vierkantor, @eric-wieser, @YaelDillies : I think Christopher is still waiting on a decision about whether or not to use `old_structure_cmd`.

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring

@mans0954 , do you want to make these changes then? If you don't have time I can knock them out for you soon. Just say the word.

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ

bors r+

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

Per the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315326.20Renaming.20is_self_adjoint), it seems that this PR is okay as-is. bors r+

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

bors r+

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

> > I have also added the `norm_one_class` and `normed_algebra` results. > > Sorry, I don't see them sweat_smile Git mistake maybe? I knew I wasn't crazy. I did do...

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

bors merge

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence

I'm okay with this as is for now. If we eventually decide that this is coming up frequently enough on bare functions and it's a pain to use then we...

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras

bors merge