Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-19 11:33 52b9b36b

View on Github →

feat(ring_theory/fractional_ideal): fractional ideal is one if and only if ideal is one (#12813)

Estimated changes

Modified src/ring_theory/fractional_ideal.lean

added theorem fractional_ideal.coe_ideal_eq_one_iff

modified theorem fractional_ideal.coe_ideal_eq_zero_iff

modified theorem fractional_ideal.coe_ideal_injective

modified theorem fractional_ideal.coe_ideal_ne_zero

modified theorem fractional_ideal.coe_ideal_ne_zero_iff