mathlib
mathlib copied to clipboard
leanprover-community
feat(analysis/normed/ring/seminorm_constructions): add seminorm_from_const
Oh, I wanted to switch the label and noticed this was tagged at WIP. I'm sorry about the premature review. I don't know why I got the GitHub notification. This is probably related to our CI experimentations.
No, you received the notification because Maria requested a review 8 hours ago.
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.
Indeed, the review request was auto-generated, but thank you very much for all the feedback, Patrick! Heather, I don't think it's ready for review yet (I need to make a PR about nonarchimedean seminorms and refactor this to use it, and I will also try to clean up the proofs following Patrick's suggestions). I will let you now when it is, thanks!
I know that I advised to use more dot notation but I didn't mean using dot notation for tendsto. Switching from tendsto f F G to F.tendsto f G doesn't save any typing and it completely messes up the reading order, suggesting that the filter F tends to the function f or something. In the same way I think that F.map f instead of map f F is really bad (and that one is unfortunately used by several people in mathlib).
