Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-09 13:51 891dfbbe

View on Github →

chore(*): clean up uses of zorn

Estimated changes

Modified analysis/metric_space.lean

Modified analysis/topology/topological_space.lean

Modified linear_algebra/basic.lean

Modified linear_algebra/basis.lean

Modified logic/schroeder_bernstein.lean

Modified order/order_iso.lean

Modified order/zorn.lean

modified theorem zorn.zorn_partial_order₀

Modified ring_theory/ideal_operations.lean

Modified ring_theory/ideals.lean