mathlib

50a8549e - Fix test: `ennreal.coe_div` is protected