Removed from mathlib

Stream: new members

[Pedro Minicz]

How often do lemmas get removed from mathlib, if at all?

[Pedro Minicz]

(Asking because I can swear two_pos : (0 : ℕ) < 2 used to exist.)

[Bryan Gin-ge Chen]

Generally we only remove redundant lemmas; not sure how often that is though, maybe a few times a week?

[Reid Barton]

See #4295

[Reid Barton]

(How to find it: git log -S two_pos)

[Bryan Gin-ge Chen]

You can also find it by searching the mathlib github repo for two_pos.

[Pedro Minicz]

Reid Barton said:

(How to find it: git log -S two_pos)

Cool. Always good to learn more git!

[Mario Carneiro]

Hm, I don't approve of removing lemmas just because they are duplicates, especially if they are explicitly aliases

[Bryan Gin-ge Chen]

It doesn't seem to me like they were explicitly aliases in this case though.

[Mario Carneiro]

I think we should be using the alias command a lot more than we do; names are hard and our naming system is not completely unambiguous

[Mario Carneiro]

in this case I think there is a clear argument for zero_lt_two and two_pos being aliases

[Scott Morrison]

Sorry, this was me. Point taken.