Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-17 17:33 f8bf0016

View on Github →

fix(ring_theory/localization): remove coe_submodule instance (#3832) This coe can loop. See zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Unknown.20error.20while.20type-checking.20with.20.60use.60/near/207089095

Estimated changes

Modified src/ring_theory/fractional_ideal.lean

modified theorem ring.fractional_ideal.coe_coe_ideal

modified theorem ring.fractional_ideal.coe_one

modified theorem ring.fractional_ideal.mem_coe

modified theorem ring.fractional_ideal.mem_zero_iff

Modified src/ring_theory/localization.lean

added def localization_map.coe_submodule

deleted theorem localization_map.mem_coe

added theorem localization_map.mem_coe_submodule