Theorem Filter.tendstoCofinite_iff_finite_preimage_singleton

Modification history

2026-03-11 00:43
Mathlib/Order/Filter/TendstoCofinite.lean
feat(RingTheory/MvPowerSeries): introduce `rename` (#33188) …
Added Filter.tendstoCofinite_iff_finite_preimage_singletonView on Github →