Theorem Filter.hasBasis_pi

Modification history

2024-08-11 11:38

Mathlib/Order/Filter/Pi.lean

chore(Filter/Pi): add missing `*` in `Type*` (#15684)

Modified Filter.hasBasis_pi View on Github →

2023-01-24 09:31

Mathlib/Order/Filter/Pi.lean

feat: port Order.Filter.Pi (#1802)

Added Filter.hasBasis_pi View on Github →