Def Filter.productSetoid

Modification history

2023-08-10 19:52

Mathlib/Order/Filter/Germ.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Filter.productSetoid View on Github →

2023-02-15 08:14

Mathlib/Order/Filter/Germ.lean

feat: port Order.Filter.Germ (#1799)

Added Filter.productSetoid View on Github →