Andrew Yang

Results 41 comments of Andrew Yang

feat: Generalize corollaries of rank-nullity theorem.

I'm busy until mid-March. I think I'll come back to this after that. Feel free to adopt if this is needed elsewhere.

feat: Generalize corollaries of rank-nullity theorem.

I tried a bit and it seems hard to separate them.

feat: Generalize corollaries of rank-nullity theorem.

Both file got longer (the +50％ file doubled in size) so I guess it's fine as long as downstream files aren't slowed?

feat: Generalize corollaries of rank-nullity theorem.

bors merge

feat: Generalize corollaries of rank-nullity theorem.

bors merge

feat(CategoryTheory/Triangulated): homological functors

Thanks! maintainer merge

feat(tactic/polyrith): solve more problems by testing for membership in the radical

I might not know what I am talking about, but it might be possible to perform some kind of binary search on the exponent in the range of say 1~64...

feat(Mathlib.Algebra.Polynomial.RingDivision): add Polynomial.nmem_nonZeroDivisors_iff

maintainer merge

feat(CategoryTheory): transport Kan extensions via equivalences

LGTM, but maybe @dagurtomas can give it a look as well?

feat(CategoryTheory): transport Kan extensions via equivalences

Thanks! (and thanks Dagur!) maintainer merge