Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 18:57 19883648

View on Github →

feat(src/ring_theory): in a PID, all fractional ideals are invertible (#2826) This would show that all PIDs are Dedekind domains, once we have a definition of Dedekind domain (we could define it right now, but it would depend on the choice of field of fractions). In localization.lean, I added a few small lemmas on localizations (localization.exists_integer_multiple and fraction_map.to_map_eq_zero_iff). @101damnations, are these additions compatible with your branches? I'm happy to change them if not.

Estimated changes

Modified src/ring_theory/fractional_ideal.lean

added theorem ring.fractional_ideal.coe_span_singleton

added theorem ring.fractional_ideal.eq_span_singleton_of_principal

added theorem ring.fractional_ideal.exists_eq_span_singleton_mul

added theorem ring.fractional_ideal.invertible_of_principal

added theorem ring.fractional_ideal.mem_coe

added theorem ring.fractional_ideal.mem_singleton_mul

added theorem ring.fractional_ideal.mul_inv_cancel_iff

added theorem ring.fractional_ideal.one_mem_one

added theorem ring.fractional_ideal.span_fractional_iff

added def ring.fractional_ideal.span_singleton

added theorem ring.fractional_ideal.span_singleton_fractional

added theorem ring.fractional_ideal.span_singleton_mul_span_singleton

added theorem ring.fractional_ideal.span_singleton_one

added theorem ring.fractional_ideal.span_singleton_zero

added theorem ring.fractional_ideal.val_coe_ideal

added theorem ring.fractional_ideal.val_inv_of_nonzero

added theorem ring.fractional_ideal.val_one

added theorem ring.fractional_ideal.val_span_singleton

Modified src/ring_theory/localization.lean

added theorem fraction_map.to_map_eq_zero_iff

added theorem localization.exists_integer_multiple'

added theorem localization.exists_integer_multiple

added theorem localization.lin_coe_apply