Commit 2023-05-23 18:30 6c2856ce

View on Github →

feat: port RingTheory.FractionalIdeal (#4243)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FractionalIdeal.lean

added theorem FractionalIdeal.add_le_add_left

added def FractionalIdeal.adjoinIntegral

added theorem FractionalIdeal.adjoinIntegral_coe

added theorem FractionalIdeal.bot_eq_zero

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 def FractionalIdeal.coeIdeal

added def FractionalIdeal.coeIdealHom

added theorem FractionalIdeal.coeIdeal_bot

added theorem FractionalIdeal.coeIdeal_eq_one

added theorem FractionalIdeal.coeIdeal_eq_zero'

added theorem FractionalIdeal.coeIdeal_eq_zero

added theorem FractionalIdeal.coeIdeal_fg

added theorem FractionalIdeal.coeIdeal_finprod

added theorem FractionalIdeal.coeIdeal_inj'

added theorem FractionalIdeal.coeIdeal_inj

added theorem FractionalIdeal.coeIdeal_injective'

added theorem FractionalIdeal.coeIdeal_injective

added theorem FractionalIdeal.coeIdeal_le_coeIdeal'

added theorem FractionalIdeal.coeIdeal_le_coeIdeal

added theorem FractionalIdeal.coeIdeal_le_one

added theorem FractionalIdeal.coeIdeal_mul

added theorem FractionalIdeal.coeIdeal_ne_one

added theorem FractionalIdeal.coeIdeal_ne_zero'

added theorem FractionalIdeal.coeIdeal_ne_zero

added theorem FractionalIdeal.coeIdeal_pow

added theorem FractionalIdeal.coeIdeal_span_singleton

added theorem FractionalIdeal.coeIdeal_sup

added theorem FractionalIdeal.coeIdeal_top

added def FractionalIdeal.coeSubmoduleHom

added theorem FractionalIdeal.coeToSet_coeToSubmodule

added def FractionalIdeal.coeToSubmodule

added theorem FractionalIdeal.coeToSubmodule_eq_bot

added theorem FractionalIdeal.coeToSubmodule_inj

added theorem FractionalIdeal.coeToSubmodule_injective

added theorem FractionalIdeal.coeToSubmodule_ne_bot

added theorem FractionalIdeal.coe_add

added theorem FractionalIdeal.coe_coeIdeal

added theorem FractionalIdeal.coe_copy

added theorem FractionalIdeal.coe_div

added theorem FractionalIdeal.coe_eq

added theorem FractionalIdeal.coe_inf

added theorem FractionalIdeal.coe_le_coe

added theorem FractionalIdeal.coe_map

added theorem FractionalIdeal.coe_mem_one

added theorem FractionalIdeal.coe_mk

added theorem FractionalIdeal.coe_mul

added theorem FractionalIdeal.coe_nat_cast

added theorem FractionalIdeal.coe_nsmul

added theorem FractionalIdeal.coe_one

added theorem FractionalIdeal.coe_one_eq_coeSubmodule_top

added theorem FractionalIdeal.coe_pow

added theorem FractionalIdeal.coe_spanSingleton

added theorem FractionalIdeal.coe_sup

added theorem FractionalIdeal.coe_zero

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_iff

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_mem_algebraMap_eq

added theorem FractionalIdeal.exists_ne_zero_mem_isInteger

added theorem FractionalIdeal.ext

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_of_le

added theorem FractionalIdeal.isFractional_of_le_one

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_one_iff_exists_coeIdeal

added theorem FractionalIdeal.le_self_mul_one_div

added theorem FractionalIdeal.le_self_mul_self

added theorem FractionalIdeal.le_spanSingleton_mul_iff

added theorem FractionalIdeal.le_zero_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_coe

added theorem FractionalIdeal.mem_coeIdeal

added theorem FractionalIdeal.mem_coeIdeal_of_mem

added theorem FractionalIdeal.mem_div_iff_of_nonzero

added theorem FractionalIdeal.mem_map

added theorem FractionalIdeal.mem_one_iff

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.mem_zero_iff

added theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal

added theorem FractionalIdeal.mul_def

added theorem FractionalIdeal.mul_div_self_cancel_iff

added theorem FractionalIdeal.mul_eq_mul

added theorem FractionalIdeal.mul_le

added theorem FractionalIdeal.mul_le_mul_left

added theorem FractionalIdeal.mul_left_mono

added theorem FractionalIdeal.mul_mem_mul

added theorem FractionalIdeal.mul_one_div_le_one

added theorem FractionalIdeal.mul_right_mono

added theorem FractionalIdeal.mul_self_le_self

added theorem FractionalIdeal.ne_zero_of_mul_eq_one

added theorem FractionalIdeal.one_div_spanSingleton

added theorem FractionalIdeal.one_le

added theorem FractionalIdeal.one_mem_one

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 FractionalIdeal.sup_eq_add

added theorem FractionalIdeal.val_eq_coe

added theorem FractionalIdeal.zero_le

added def FractionalIdeal

added theorem Ideal.fg_of_isUnit

added theorem IsFractional.div_of_nonzero

added theorem IsFractional.inf_right

added theorem IsFractional.map

added theorem IsFractional.mul

added theorem IsFractional.nsmul

added theorem IsFractional.pow

added theorem IsFractional.sup

added def IsFractional