mathlib3
c48d7bfe - feat(data/real/enat_ennreal): define coercion from `enat` to `ennreal` (#17207)

Commit

3 years ago

feat(data/real/enat_ennreal): define coercion from `enat` to `ennreal` (#17207)

Author

urkud

urkud

Parents

Loading