Commit 2023-01-09 19:56 2f588be3

View on Github →

refactor(ring_theory/fractional_ideal): refactor coe_to_fractional_ideal lemmas (#18055) Rename coe_to_fractional_ideal lemmas to coe_ideal' lemmas and extract coe_ideal_inj as standalone eq_iff lemmas.

Estimated changes

Modified src/ring_theory/class_group.lean

modified theorem card_class_group_eq_one

modified theorem class_group.mk0_eq_one_iff

Modified src/ring_theory/dedekind_domain/factorization.lean

Modified src/ring_theory/dedekind_domain/ideal.lean

Modified src/ring_theory/fractional_ideal.lean

added theorem fractional_ideal.coe_ideal_bot

added theorem fractional_ideal.coe_ideal_eq_one

deleted theorem fractional_ideal.coe_ideal_eq_one_iff

added theorem fractional_ideal.coe_ideal_eq_zero'

added theorem fractional_ideal.coe_ideal_eq_zero

deleted theorem fractional_ideal.coe_ideal_eq_zero_iff

added theorem fractional_ideal.coe_ideal_inj'

added theorem fractional_ideal.coe_ideal_inj

added theorem fractional_ideal.coe_ideal_injective'

added theorem fractional_ideal.coe_ideal_ne_one

added theorem fractional_ideal.coe_ideal_ne_zero'

modified theorem fractional_ideal.coe_ideal_ne_zero

deleted theorem fractional_ideal.coe_ideal_ne_zero_iff

modified theorem fractional_ideal.coe_ideal_top

deleted theorem fractional_ideal.coe_to_fractional_ideal_bot

deleted theorem fractional_ideal.coe_to_fractional_ideal_eq_zero

deleted theorem fractional_ideal.coe_to_fractional_ideal_injective

deleted theorem fractional_ideal.coe_to_fractional_ideal_ne_zero

added theorem fractional_ideal.coe_to_submodule_inj

modified theorem fractional_ideal.is_fractional_of_le

modified theorem fractional_ideal.is_fractional_of_le_one

added theorem fractional_ideal.is_noetherian_coe_ideal

deleted theorem fractional_ideal.is_noetherian_coe_to_fractional_ideal