Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-09 15:55 d78c8ea2

View on Github →

chore(ring_theory): cleaned up ideals

Estimated changes

Modified analysis/topology/topological_structures.lean

Modified data/set/basic.lean

added theorem set.exists_of_ssubset

Modified logic/basic.lean

added theorem classical.or_iff_not_imp_left

added theorem classical.or_iff_not_imp_right

Modified order/filter.lean

Modified order/zorn.lean

Modified ring_theory/ideals.lean

modified theorem is_maximal_ideal.mk

modified def local_of_nonunits_ideal

modified theorem not_unit_of_mem_maximal_ideal

Modified ring_theory/localization.lean