Style: Add Deprecation sub-section

[vlad902]

Zulip thread here:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Style.20guide.3A.20deprecation

[jcommelin]

Thanks for documenting this!

[jcommelin]

Suggested change

	that rely on these definitions to fail to compile. Any publicly exposed theorem
	definitions that are being changed should be gracefully transitioned by keeping the
	that rely on these definitions to fail to compile. Any publicly exposed theorem and
	definitions that are being changed should be gracefully transitioned by keeping the

"change" is maybe a bit ambiguous: if I weaken an assumption? Or change an implicit variable to explicit, etc...

If the name doesn't change, it is also hard to use the deprecated attribute.

[vlad902]

That's a good point. I've updated the wording to say:

Any publicly exposed theorems and definitions that are being removed should be ...