lean core vs mathlib

Stream: general

[Kenny Lau]

What is the criterion for a definition / theorem to be put in mathlib vs in lean core?

[Kevin Buzzard]

Does it have to be in core if it's needed to make the core unit tests work?

[Mario Carneiro]

well yes, although you could remove the tests

[Kevin Buzzard]

You once told me that this was like breaking the code and then covering your tracks