mathlib

c4a32e72 - doc(topology/uniform_space/basic): library note on forgetful inheritance (#3070)

doc(topology/uniform_space/basic): library note on forgetful inheritance (#3070) A (long) library note explaining design decisions related to forgetful inheritance, and reference to this note in various places (I have probably forgotten a few of them).