Def DiscreteQuotient.ofLe

Modification history

2023-04-17 12:04

Mathlib/Topology/DiscreteQuotient.lean

chore: fix names in DiscreteQuotient (#3481)

Deleted DiscreteQuotient.ofLe View on Github →

2023-02-11 07:51

Mathlib/Topology/DiscreteQuotient.lean

feat: port Topology.DiscreteQuotient (#2157) …

Added DiscreteQuotient.ofLe View on Github →