mathlib

a0ba5e7d - doc(data/real/*): add a few docstrings, `ereal.has_zero`, and `ereal.inhabited` (#4378)