mathlib

5287b4ab - make semantics clearer and remove reference