mathlib3
ad67d314 - Renaming hyperfilter to free_ultrafilter

Commit

3 years ago

Renaming hyperfilter to free_ultrafilter The standard terminology is free ultrafilter.

References

Author

berndlosert

Parents