Commit 2024-01-31 10:21 bb85b99d

View on Github →

feat: fix typo (eventually_nhds_subtype_if -> eventually_nhds_subtype_iff) (#10124) This was unnoticed during the review of #7568

Estimated changes