Commit 2021-01-06 11:04 35ff0434

View on Github →

feat(ring_theory/fractional_ideal): move inv to dedekind_domain (#5053) Remove all instances of inv and I^{-1}. The notation (1 / I) is the one used for the old I^{-1}.

Estimated changes

Modified src/ring_theory/dedekind_domain.lean

added theorem coe_inv_of_nonzero

added theorem inv_eq

added theorem inv_nonzero

added theorem inv_zero'

added theorem invertible_iff_generator_nonzero

added theorem invertible_of_principal

added theorem is_principal_inv

added theorem map_inv

added theorem mul_generator_self_inv

added theorem mul_inv_cancel_iff

added theorem right_inverse_eq

added theorem span_singleton_inv

Modified src/ring_theory/fractional_ideal.lean

deleted theorem ring.fractional_ideal.coe_inv_of_nonzero

modified theorem ring.fractional_ideal.div_span_singleton

added theorem ring.fractional_ideal.eq_one_div_of_mul_eq_one

deleted theorem ring.fractional_ideal.inv_eq

deleted theorem ring.fractional_ideal.inv_nonzero

deleted theorem ring.fractional_ideal.inv_zero

deleted theorem ring.fractional_ideal.invertible_iff_generator_nonzero

deleted theorem ring.fractional_ideal.invertible_of_principal

modified theorem ring.fractional_ideal.is_noetherian

added theorem ring.fractional_ideal.is_noetherian_span_singleton_inv_to_map_mul

deleted theorem ring.fractional_ideal.is_noetherian_span_singleton_to_map_inv_mul

deleted theorem ring.fractional_ideal.is_principal_inv

deleted theorem ring.fractional_ideal.map_inv

added theorem ring.fractional_ideal.map_one_div

added theorem ring.fractional_ideal.mul_div_self_cancel_iff

deleted theorem ring.fractional_ideal.mul_generator_self_inv

deleted theorem ring.fractional_ideal.mul_inv_cancel_iff

deleted theorem ring.fractional_ideal.right_inverse_eq

deleted theorem ring.fractional_ideal.span_singleton_inv