Andrew Yang

Results 78 comments of Andrew Yang

feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem

What is the status of this PR? It seems to me that you might have forgot to push your commit.

feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem

I think that is exactly `Filter.Tendsto.congr'`

feat: presented monoids

Also please merge master in case of merge conflicts. Thanks!

feat: presented monoids

Hey sorry for abandoning this for so long. I agree with Yael that the more useful part are the monoid API and I might not be the best person to...

feat: presented monoids

LGTM Thanks! maintainer merge

feat(Algebra): characterise when a submodule constructor is equal to `⊥`

Can you point me to somewhere that this is needed? Is it possible to just add `SetLike.ext_iff` into your simp call? I am not that sure if we want this...

feat(Algebra): characterise when a submodule constructor is equal to `⊥`

I do not think they are analogous. Coercion and `mk` are different. I don't think we in general should be stating lemmas about `mk` or should be seeing `mk` at...

feat(Algebra): characterise when a submodule constructor is equal to `⊥`

And can you add the analogous lemmas for `top`? Thanks.