mathlib

af38b5cd - add forgetful functor, show it reflects isos