Commit 2024-01-19 16:41 de9c7b5b

View on Github →

chore: Split RingTheory.FractionalIdeal.Basic (#9854) The file RingTheory.FractionalIdeal.Basic is more than 1600 lines long. This PR splits it into two files: Basic and Operations following the model of RingTheory.Ideal.Basic and RingTheory.Ideal.Operations

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

deleted def FractionalIdeal.adjoinIntegral

deleted theorem FractionalIdeal.adjoinIntegral_coe

deleted theorem FractionalIdeal.canonicalEquiv_canonicalEquiv

deleted theorem FractionalIdeal.canonicalEquiv_coeIdeal

deleted theorem FractionalIdeal.canonicalEquiv_flip

deleted theorem FractionalIdeal.canonicalEquiv_self

deleted theorem FractionalIdeal.canonicalEquiv_spanSingleton

deleted theorem FractionalIdeal.canonicalEquiv_symm

deleted theorem FractionalIdeal.canonicalEquiv_trans_canonicalEquiv

deleted theorem FractionalIdeal.coeFun_mapEquiv

deleted theorem FractionalIdeal.coeIdeal_eq_one

deleted theorem FractionalIdeal.coeIdeal_eq_zero

deleted theorem FractionalIdeal.coeIdeal_fg

deleted theorem FractionalIdeal.coeIdeal_inj

deleted theorem FractionalIdeal.coeIdeal_injective

deleted theorem FractionalIdeal.coeIdeal_ne_one

deleted theorem FractionalIdeal.coeIdeal_ne_zero

deleted theorem FractionalIdeal.coeIdeal_span_singleton

deleted theorem FractionalIdeal.coe_div

deleted theorem FractionalIdeal.coe_map

deleted theorem FractionalIdeal.coe_spanSingleton

deleted theorem FractionalIdeal.den_mul_self_eq_num'

deleted theorem FractionalIdeal.div_nonzero

deleted theorem FractionalIdeal.div_one

deleted theorem FractionalIdeal.div_spanSingleton

deleted theorem FractionalIdeal.div_zero

deleted theorem FractionalIdeal.eq_one_div_of_mul_eq_one_right

deleted theorem FractionalIdeal.eq_spanSingleton_mul

deleted theorem FractionalIdeal.eq_spanSingleton_of_principal

deleted theorem FractionalIdeal.eq_zero_or_one

deleted theorem FractionalIdeal.eq_zero_or_one_of_isField

deleted theorem FractionalIdeal.exists_eq_spanSingleton_mul

deleted theorem FractionalIdeal.exists_ne_zero_mem_isInteger

deleted theorem FractionalIdeal.fg_of_isUnit

deleted theorem FractionalIdeal.fg_unit

deleted theorem FractionalIdeal.fractional_div_of_nonzero

deleted theorem FractionalIdeal.isFractional_adjoin_integral

deleted theorem FractionalIdeal.isFractional_of_fg

deleted theorem FractionalIdeal.isFractional_span_iff

deleted theorem FractionalIdeal.isFractional_span_singleton

deleted theorem FractionalIdeal.isNoetherian

deleted theorem FractionalIdeal.isNoetherian_coeIdeal

deleted theorem FractionalIdeal.isNoetherian_iff

deleted theorem FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul

deleted theorem FractionalIdeal.isNoetherian_zero

deleted theorem FractionalIdeal.isPrincipal_iff

deleted theorem FractionalIdeal.le_div_iff_mul_le

deleted theorem FractionalIdeal.le_div_iff_of_nonzero

deleted theorem FractionalIdeal.le_self_mul_one_div

deleted theorem FractionalIdeal.le_spanSingleton_mul_iff

deleted def FractionalIdeal.map

deleted def FractionalIdeal.mapEquiv

deleted theorem FractionalIdeal.mapEquiv_apply

deleted theorem FractionalIdeal.mapEquiv_refl

deleted theorem FractionalIdeal.mapEquiv_symm

deleted theorem FractionalIdeal.map_add

deleted theorem FractionalIdeal.map_coeIdeal

deleted theorem FractionalIdeal.map_comp

deleted theorem FractionalIdeal.map_div

deleted theorem FractionalIdeal.map_eq_zero_iff

deleted theorem FractionalIdeal.map_id

deleted theorem FractionalIdeal.map_injective

deleted theorem FractionalIdeal.map_map_symm

deleted theorem FractionalIdeal.map_mem_map

deleted theorem FractionalIdeal.map_mul

deleted theorem FractionalIdeal.map_ne_zero

deleted theorem FractionalIdeal.map_one

deleted theorem FractionalIdeal.map_one_div

deleted theorem FractionalIdeal.map_symm_map

deleted theorem FractionalIdeal.map_zero

deleted theorem FractionalIdeal.mem_adjoinIntegral_self

deleted theorem FractionalIdeal.mem_canonicalEquiv_apply

deleted theorem FractionalIdeal.mem_div_iff_of_nonzero

deleted theorem FractionalIdeal.mem_map

deleted theorem FractionalIdeal.mem_singleton_mul

deleted theorem FractionalIdeal.mem_spanSingleton

deleted theorem FractionalIdeal.mem_spanSingleton_self

deleted theorem FractionalIdeal.mem_span_mul_finite_of_mem_mul

deleted theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal

deleted theorem FractionalIdeal.mul_div_self_cancel_iff

deleted theorem FractionalIdeal.mul_one_div_le_one

deleted theorem FractionalIdeal.ne_zero_of_mul_eq_one

deleted theorem FractionalIdeal.one_div_spanSingleton

deleted def FractionalIdeal.spanFinset

deleted theorem FractionalIdeal.spanFinset_coe

deleted theorem FractionalIdeal.spanFinset_eq_zero

deleted theorem FractionalIdeal.spanFinset_ne_zero

deleted theorem FractionalIdeal.spanSingleton_eq_spanSingleton

deleted theorem FractionalIdeal.spanSingleton_eq_zero_iff

deleted theorem FractionalIdeal.spanSingleton_le_iff_mem

deleted theorem FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal

deleted theorem FractionalIdeal.spanSingleton_mul_le_iff

deleted theorem FractionalIdeal.spanSingleton_mul_spanSingleton

deleted theorem FractionalIdeal.spanSingleton_ne_zero_iff

deleted theorem FractionalIdeal.spanSingleton_one

deleted theorem FractionalIdeal.spanSingleton_pow

deleted theorem FractionalIdeal.spanSingleton_zero

deleted theorem Ideal.fg_of_isUnit

deleted theorem IsFractional.div_of_nonzero

deleted theorem IsFractional.map

Created Mathlib/RingTheory/FractionalIdeal/Operations.lean

added def FractionalIdeal.adjoinIntegral

added theorem FractionalIdeal.adjoinIntegral_coe

added theorem FractionalIdeal.canonicalEquiv_canonicalEquiv

added theorem FractionalIdeal.canonicalEquiv_coeIdeal

added theorem FractionalIdeal.canonicalEquiv_flip

added theorem FractionalIdeal.canonicalEquiv_self

added theorem FractionalIdeal.canonicalEquiv_spanSingleton

added theorem FractionalIdeal.canonicalEquiv_symm

added theorem FractionalIdeal.canonicalEquiv_trans_canonicalEquiv

added theorem FractionalIdeal.coeFun_mapEquiv

added theorem FractionalIdeal.coeIdeal_eq_one

added theorem FractionalIdeal.coeIdeal_eq_zero

added theorem FractionalIdeal.coeIdeal_fg

added theorem FractionalIdeal.coeIdeal_inj

added theorem FractionalIdeal.coeIdeal_injective

added theorem FractionalIdeal.coeIdeal_ne_one

added theorem FractionalIdeal.coeIdeal_ne_zero

added theorem FractionalIdeal.coeIdeal_span_singleton

added theorem FractionalIdeal.coe_div

added theorem FractionalIdeal.coe_map

added theorem FractionalIdeal.coe_spanSingleton

added theorem FractionalIdeal.den_mul_self_eq_num'

added theorem FractionalIdeal.div_nonzero

added theorem FractionalIdeal.div_one

added theorem FractionalIdeal.div_spanSingleton

added theorem FractionalIdeal.div_zero

added theorem FractionalIdeal.eq_one_div_of_mul_eq_one_right

added theorem FractionalIdeal.eq_spanSingleton_mul

added theorem FractionalIdeal.eq_spanSingleton_of_principal

added theorem FractionalIdeal.eq_zero_or_one

added theorem FractionalIdeal.eq_zero_or_one_of_isField

added theorem FractionalIdeal.exists_eq_spanSingleton_mul

added theorem FractionalIdeal.exists_ne_zero_mem_isInteger

added theorem FractionalIdeal.fg_of_isUnit

added theorem FractionalIdeal.fg_unit

added theorem FractionalIdeal.fractional_div_of_nonzero

added theorem FractionalIdeal.isFractional_adjoin_integral

added theorem FractionalIdeal.isFractional_of_fg

added theorem FractionalIdeal.isFractional_span_iff

added theorem FractionalIdeal.isFractional_span_singleton

added theorem FractionalIdeal.isNoetherian

added theorem FractionalIdeal.isNoetherian_coeIdeal

added theorem FractionalIdeal.isNoetherian_iff

added theorem FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul

added theorem FractionalIdeal.isNoetherian_zero

added theorem FractionalIdeal.isPrincipal_iff

added theorem FractionalIdeal.le_div_iff_mul_le

added theorem FractionalIdeal.le_div_iff_of_nonzero

added theorem FractionalIdeal.le_self_mul_one_div

added theorem FractionalIdeal.le_spanSingleton_mul_iff

added def FractionalIdeal.map

added def FractionalIdeal.mapEquiv

added theorem FractionalIdeal.mapEquiv_apply

added theorem FractionalIdeal.mapEquiv_refl

added theorem FractionalIdeal.mapEquiv_symm

added theorem FractionalIdeal.map_add

added theorem FractionalIdeal.map_coeIdeal

added theorem FractionalIdeal.map_comp

added theorem FractionalIdeal.map_div

added theorem FractionalIdeal.map_eq_zero_iff

added theorem FractionalIdeal.map_id

added theorem FractionalIdeal.map_injective

added theorem FractionalIdeal.map_map_symm

added theorem FractionalIdeal.map_mem_map

added theorem FractionalIdeal.map_mul

added theorem FractionalIdeal.map_ne_zero

added theorem FractionalIdeal.map_one

added theorem FractionalIdeal.map_one_div

added theorem FractionalIdeal.map_symm_map

added theorem FractionalIdeal.map_zero

added theorem FractionalIdeal.mem_adjoinIntegral_self

added theorem FractionalIdeal.mem_canonicalEquiv_apply

added theorem FractionalIdeal.mem_div_iff_of_nonzero

added theorem FractionalIdeal.mem_map

added theorem FractionalIdeal.mem_singleton_mul

added theorem FractionalIdeal.mem_spanSingleton

added theorem FractionalIdeal.mem_spanSingleton_self

added theorem FractionalIdeal.mem_span_mul_finite_of_mem_mul

added theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal

added theorem FractionalIdeal.mul_div_self_cancel_iff

added theorem FractionalIdeal.mul_one_div_le_one

added theorem FractionalIdeal.ne_zero_of_mul_eq_one

added theorem FractionalIdeal.one_div_spanSingleton

added def FractionalIdeal.spanFinset

added theorem FractionalIdeal.spanFinset_coe

added theorem FractionalIdeal.spanFinset_eq_zero

added theorem FractionalIdeal.spanFinset_ne_zero

added theorem FractionalIdeal.spanSingleton_eq_spanSingleton

added theorem FractionalIdeal.spanSingleton_eq_zero_iff

added theorem FractionalIdeal.spanSingleton_le_iff_mem

added theorem FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal

added theorem FractionalIdeal.spanSingleton_mul_le_iff

added theorem FractionalIdeal.spanSingleton_mul_spanSingleton

added theorem FractionalIdeal.spanSingleton_ne_zero_iff

added theorem FractionalIdeal.spanSingleton_one

added theorem FractionalIdeal.spanSingleton_pow

added theorem FractionalIdeal.spanSingleton_zero

added theorem Ideal.fg_of_isUnit

added theorem IsFractional.div_of_nonzero

added theorem IsFractional.map