mathlib

mathlib copied to clipboard

feat(ring_theory/derivation): Endomorphisms of the Kähler differential module

1

--- - [x] depends on: #15855 - [x] depends on: #15856 - [ ] depends on: #16047 [](https://gitpod.io/from-referrer/)

erdOne

--- [](https://gitpod.io/from-referrer/)

erdOne

--- [](https://gitpod.io/from-referrer/)

erdOne

feat(logic/basic): given two different elements, one of the two is different from a third

3

This lemma is extracted from #15984, as suggested by the code-review. --- [](https://gitpod.io/from-referrer/)

adomani

feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism.

2

--- [](https://gitpod.io/from-referrer/)

erdOne

chore(*): restore `subsingleton` instances and remove hacks

1

#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances...

alreadydone

I just open this to track my progress and let everyone know how I plan to do this. This is very tedious, so if anyone wants to help I would...

mcdoll

feat(representation_theory/character): orthogonality of characters

1

Orthogonality of characters for representations of finite groups - [ ] depends on: #13789 - [ ] depends on: #13794 --- [](https://gitpod.io/from-referrer/)

antoinelab01

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros

5

Local version: an analytic function is either locally zero, or nonzero in a punctured neighborhood. --- Second take on #14382 but starting from scratch. [](https://gitpod.io/from-referrer/)

vbeffara

--- [](https://gitpod.io/from-referrer/)

TwoFX