Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-02 14:48 c3442db1

View on Github →

chore(ring_theory/dedekind_domain/ideal): remove fractional_ideal in open namespaces (#18033)

Estimated changes

Modified src/ring_theory/dedekind_domain/ideal.lean

modified theorem fractional_ideal.coe_ideal_le_self_mul_inv

modified theorem fractional_ideal.inv_anti_mono

modified theorem fractional_ideal.inv_zero'

modified theorem fractional_ideal.mem_inv_iff

modified theorem fractional_ideal.mul_inv_cancel_iff

modified theorem fractional_ideal.mul_inv_cancel_iff_is_unit

modified theorem fractional_ideal.right_inverse_eq

modified theorem fractional_ideal.span_singleton_inv

Modified src/ring_theory/fractional_ideal.lean

modified def fractional_ideal.span_finset