| Name | Category | Theorems |
|---|
coeIdeal 📖 | CompOp | 69 mathmath: coeIdeal_top, finprod_heightOneSpectrum_factorization_principal, coeIdealHom_apply, coeIdeal_span_singleton, coe_coeIdeal, coeIdeal_fg, count_finsuppProd, coeIdeal_le_one, extendedHomₐ_coeIdeal_eq_map, mk'_mul_coeIdeal_eq_coeIdeal, coeIdeal_inj, isNoetherian_coeIdeal, isUnit_num, count_coe_nonneg, count_finprod_coprime, coeIdeal_sup, le_one_iff_exists_coeIdeal, count_finprod, count_ne_zero, coeIdeal_inf, differentialIdeal_le_iff, map_coeIdeal, coeIdeal_differentIdeal, coeIdeal_le_coeIdeal', extended_coeIdeal_eq_map, coe_ideal_span_singleton_div_self, count_maximal_coprime, num_le_mul_inv, mem_coeIdeal, coeIdeal_injective, coeIdeal_eq_zero', coeIdeal_mul, canonicalEquiv_coeIdeal, differentialIdeal_le_fractionalIdeal_iff, mem_coeIdeal_of_mem, coeIdeal_eq_one, one_mem_inv_coe_ideal, coe_ideal_mul_inv, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, Ideal.finite_mulSupport_coe, coeIdeal_inj', coeIdeal_bot, count_zpow_self, coe_ideal_span_singleton_inv_mul, spanSingleton_mul_coeIdeal_eq_coeIdeal, coeIdeal_eq_zero, not_inv_le_one_of_ne_bot, exists_eq_spanSingleton_mul, count_pow_self, Ideal.finprod_heightOneSpectrum_factorization_coe, Ideal.exist_integer_multiples_notMem, coe_ideal_span_singleton_mul_inv, count_self, den_mul_self_eq_num', WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, coeIdeal_absNorm, count_maximal, coeIdeal_injective', finprod_heightOneSpectrum_factorization_principal_fraction, Ideal.finite_mulSupport_inv, coe_mk0, num_le, coeIdeal_pow, count_coe, coe_ideal_le_self_mul_inv, finprod_heightOneSpectrum_factorization', exists_notMem_one_of_ne_bot, coeIdeal_finprod, coeIdeal_le_coeIdeal
|
coeIdealHom 📖 | CompOp | 1 mathmath: coeIdealHom_apply
|
coeSubmoduleHom 📖 | CompOp | 1 mathmath: coeSubmoduleHom_apply
|
coeToSubmodule 📖 | CompOp | 76 mathmath: fg_of_isUnit, isPrincipal_of_isPrincipal_num, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, coe_coeIdeal, fg_unit, coeIdeal_fg, isFractional_div_of_ne_zero, coe_le_coe, coe_extendedHomₐ_eq_span, coe_inf, isNoetherian_coeIdeal, inv_nonzero, div_of_ne_zero, coe_pow, fractional_div_of_nonzero, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, coe_nsmul, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, coe_natCast, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.span_idealLatticeBasis, coe_dual, differentialIdeal_le_iff, div_nonzero, coeToSubmodule_eq_bot, adjoinIntegral_coe, coe_dual_one, coeToSubmodule_inj, coe_ext_iff, fg_of_isNoetherianRing, mul_generator_self_inv, coe_mk, isNoetherian_spanSingleton_inv_to_map_mul, coe_add, coe_one_eq_coeSubmodule_top, isPrincipal_iff, coe_inv_of_ne_zero, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, isNoetherian_zero, coe_one, differentialIdeal_le_fractionalIdeal_iff, coe_mul, mul_def, coeSubmoduleHom_apply, coeToSet_coeToSubmodule, ClassGroup.mk_eq_one_iff, NumberField.fractionalIdeal_rank, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, eq_spanSingleton_of_principal, den_mul_self_eq_num, coe_map, isNoetherian_iff, coe_sup, isFractional, coe_inv_of_nonzero, spanFinset_coe, NumberField.mem_span_basisOfFractionalIdeal, isPrincipal.of_finite_maximals_of_inv, mul_def', ClassGroup.isPrincipal_coeSubmodule_of_isUnit, mem_coe, coeToSubmodule_injective, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, abs_det_basis_change, coe_spanSingleton, val_eq_coe, isNoetherian, NumberField.basisOfFractionalIdeal_apply, isPrincipal, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, equivNum_apply, coe_div, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, inv_of_ne_zero, coe_zero, coe_extended_eq_span
|
commSemiring 📖 | CompOp | 58 mathmath: finprod_heightOneSpectrum_factorization_principal, ClassGroup.mk0_integralRep, coeIdealHom_apply, ClassGroup.Quot_mk_eq_mk, fg_unit, coe_extendedHomₐ_eq_span, mem_principal_ideals_iff, absNorm_eq', count_finsuppProd, extendedHomₐ_coeIdeal_eq_map, isUnit_num, extendedHom_apply, dual_eq_dual_mul_dual, count_finprod_coprime, finprod_heightOneSpectrum_factorization, coe_toPrincipalIdeal, count_prod, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, count_finprod, NumberField.det_basisOfFractionalIdeal_eq_absNorm, absNorm_bot, extendedHomₐ_injective, PrincipalIdeals.normal, NumberField.mixedEmbedding.covolume_idealLattice, extendedHomₐ_eq_zero_iff, extendedHomₐ_eq_one_iff, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, absNorm_eq, coeSubmoduleHom_apply, absNorm_span_singleton, ClassGroup.mk_mk0, ClassGroup.mk_eq_one_iff, toPrincipalIdeal_eq_iff, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', ClassGroup.mk_eq_mk, WeierstrassCurve.Affine.Point.toClass_some, instIsOrderedRing, absNorm_nonneg, one_le_extendedHomₐ_iff, mul_inv_cancel_iff_isUnit, abs_det_basis_change, Ideal.finprod_heightOneSpectrum_factorization_coe, toPrincipalIdeal_def, ClassGroup.equiv_mk0, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, ClassGroup.mk_canonicalEquiv, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, coeIdeal_absNorm, finprod_heightOneSpectrum_factorization_principal_fraction, absNorm_eq_zero_iff, ClassGroup.mk_def, WeierstrassCurve.Affine.Point.toClass_apply, ClassGroup.equiv_mk, extendedHomₐ_le_one_iff, finprod_heightOneSpectrum_factorization', coeIdeal_finprod, absNorm_one
|
copy 📖 | CompOp | 2 mathmath: coe_eq, coe_copy
|
den 📖 | CompOp | 6 mathmath: absNorm_eq, den_mul_self_eq_num, absNorm_div_norm_eq_absNorm_div_norm, equivNum_apply, den_mul_self_eq_num', den_mem_inv
|
equivNum 📖 | CompOp | 1 mathmath: equivNum_apply
|
equivNumOfIsLocalization 📖 | CompOp | — |
equivNumOfIsSMulRegular 📖 | CompOp | — |
instAdd 📖 | CompOp | 27 mathmath: canonicalEquiv_trans_canonicalEquiv, mapEquiv_apply, sup_eq_add, mapEquiv_symm, canonicalEquiv_symm, coeIdeal_sup, mem_add, canonicalEquiv_mk0, canonicalEquiv_spanSingleton, coe_add, canonicalEquiv_coeIdeal, coeFun_mapEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_flip, extended_add, divMod_spec, IsDedekindDomain.exists_add_spanSingleton_mul_eq, map_canonicalEquiv_mk0, mem_canonicalEquiv_apply, mapEquiv_refl, map_add, canonicalEquiv_self, ClassGroup.mk_canonicalEquiv, instCanonicallyOrderedAdd, add_le_add_left, ClassGroup.mk_def, ClassGroup.equiv_mk
|
instCoeOutSubmodule 📖 | CompOp | — |
instCoeTCIdeal 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instMax 📖 | CompOp | 3 mathmath: sup_eq_add, sup_mul_inf, coe_sup
|
instMin 📖 | CompOp | 5 mathmath: sup_mul_inf, coe_inf, inf_mul, coeIdeal_inf, mul_inf
|
instModuleSubtypeMemSubmoduleCoeToSubmodule 📖 | CompOp | 5 mathmath: isNoetherian_coeIdeal, isNoetherian_spanSingleton_inv_to_map_mul, isNoetherian_zero, isNoetherian_iff, isNoetherian
|
instMul 📖 | CompOp | 89 mathmath: le_spanSingleton_mul_iff, canonicalEquiv_trans_canonicalEquiv, spanSingleton_inv_mul, spanSingleton_mul_inv, mapEquiv_apply, mul_eq_mul, le_dual_iff, sup_mul_inf, invertible_of_principal, instMulPosStrictMonoNonZeroDivisors, le_div_iff_mul_le, mk'_mul_coeIdeal_eq_coeIdeal, inf_mul, spanSingleton_mul_spanSingleton, le_self_mul_inv, instMulPosReflectLENonZeroDivisors, mapEquiv_symm, dual_eq_dual_mul_dual, canonicalEquiv_symm, mul_right_mono, mul_inv_cancel, count_ne_zero, spanSingleton_mul_le_iff, mul_left_strictMono, canonicalEquiv_mk0, div_eq_mul_inv, mul_generator_self_inv, isNoetherian_spanSingleton_inv_to_map_mul, canonicalEquiv_spanSingleton, eq_spanSingleton_mul, IsDedekindDomainInv.mul_inv_eq_one, extended_mul, num_le_mul_inv, coeIdeal_mul, dual_mul_self, canonicalEquiv_coeIdeal, coe_mul, mul_def, coeFun_mapEquiv, dual_eq_mul_inv, mul_le, count_mul, mul_one_div_le_one, canonicalEquiv_canonicalEquiv, mul_le_mul_left, coe_ideal_mul_inv, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, mul_left_mono, instMulRightMono, canonicalEquiv_flip, mul_left_le_iff, map_mul, mul_inv_cancel_iff, coe_ideal_span_singleton_inv_mul, mul_inf, spanSingleton_mul_coeIdeal_eq_coeIdeal, div_spanSingleton, IsDedekindDomainInv.inv_mul_eq_one, mem_singleton_mul, le_self_mul_one_div, dual_inv, mul_right_le_iff, divMod_spec, bot_lt_mul_inv, IsDedekindDomain.exists_add_spanSingleton_mul_eq, mul_inv_cancel_iff_isUnit, instPosMulStrictMonoNonZeroDivisors, exists_eq_spanSingleton_mul, mul_self_le_self, map_canonicalEquiv_mk0, mem_canonicalEquiv_apply, mapEquiv_refl, invertible_iff_generator_nonzero, count_mul', le_self_mul_self, instMulLeftMono, coe_ideal_span_singleton_mul_inv, den_mul_self_eq_num', canonicalEquiv_self, mul_mem_mul, self_mul_dual, ClassGroup.mk_canonicalEquiv, ClassGroup.mk_def, isDedekindDomainInv_iff, mul_right_strictMono, coe_ideal_le_self_mul_inv, instPosMulReflectLENonZeroDivisors, ClassGroup.equiv_mk, mul_div_self_cancel_iff
|
instNatCast 📖 | CompOp | 1 mathmath: coe_natCast
|
instOne 📖 | CompOp | 59 mathmath: coeIdeal_top, spanSingleton_inv_mul, spanSingleton_mul_inv, map_one_div, le_dual_iff, one_mem_one, invertible_of_principal, one_le, coe_mem_one, coeIdeal_le_one, div_one, eq_zero_or_one_of_isField, inv_nonzero, inv_eq, dual_eq_dual_mul_dual, one_div_spanSingleton, one_le_dual_one, mul_inv_cancel, le_one_iff_exists_coeIdeal, mem_one_iff, coe_dual_one, coeIdeal_differentIdeal, coe_ideal_span_singleton_div_self, mul_generator_self_inv, IsDedekindDomainInv.mul_inv_eq_one, coe_one_eq_coeSubmodule_top, extendedHomₐ_eq_one_iff, coe_one, dual_mul_self, extended_one, dual_eq_mul_inv, mul_one_div_le_one, coeIdeal_eq_one, coe_ideal_mul_inv, Ideal.finite_mulSupport_coe, map_one, mul_inv_cancel_iff, coe_ideal_span_singleton_inv_mul, count_one, IsDedekindDomainInv.inv_mul_eq_one, one_le_extendedHomₐ_iff, dual_inv, not_inv_le_one_of_ne_bot, mul_inv_cancel_iff_isUnit, eq_zero_or_one, invertible_iff_generator_nonzero, spanSingleton_one, spanSingleton_div_self, coe_ideal_span_singleton_mul_inv, self_mul_dual, adjoinIntegral_eq_one_of_isUnit, Ideal.finite_mulSupport_inv, isDedekindDomainInv_iff, extendedHomₐ_le_one_iff, mem_inv_iff, inv_of_ne_zero, mul_div_self_cancel_iff, exists_notMem_one_of_ne_bot, absNorm_one
|
instPartialOrder 📖 | CompOp | 48 mathmath: le_spanSingleton_mul_iff, le_dual_iff, coe_le_coe, one_le, coeIdeal_le_one, inv_le_inv_iff, instMulPosStrictMonoNonZeroDivisors, le_div_iff_mul_le, le_div_iff_of_ne_zero, instMulPosReflectLENonZeroDivisors, le_div_iff_of_nonzero, le_zero_iff, spanSingleton_le_iff_mem, mul_right_mono, one_le_dual_one, le_one_iff_exists_coeIdeal, spanSingleton_mul_le_iff, absNorm_bot, mul_left_strictMono, inv_le_dual, coeIdeal_le_coeIdeal', le_inv_comm, num_le_mul_inv, bot_eq_zero, differentialIdeal_le_fractionalIdeal_iff, mul_le, mul_one_div_le_one, mul_left_mono, instMulRightMono, dual_le_dual, mul_left_le_iff, instIsOrderedRing, one_le_extendedHomₐ_iff, mul_right_le_iff, bot_lt_mul_inv, not_inv_le_one_of_ne_bot, instPosMulStrictMonoNonZeroDivisors, zero_le, dual_inv_le, instMulLeftMono, inv_le_comm, instCanonicallyOrderedAdd, num_le, mul_right_strictMono, coe_ideal_le_self_mul_inv, instPosMulReflectLENonZeroDivisors, extendedHomₐ_le_one_iff, coeIdeal_le_coeIdeal
|
instPowNat 📖 | CompOp | 5 mathmath: coe_pow, spanSingleton_pow, count_pow, count_pow_self, coeIdeal_pow
|
instSMulNat 📖 | CompOp | 1 mathmath: coe_nsmul
|
instSetLike 📖 | CompOp | 46 mathmath: le_spanSingleton_mul_iff, mem_adjoinIntegral_self, NumberField.mixedEmbedding.mem_idealLattice, one_mem_one, coe_extendedHomₐ_eq_span, one_le, coe_mem_one, le_div_iff_of_ne_zero, le_div_iff_of_nonzero, mem_div_iff_of_nonzero, mem_map, spanSingleton_le_iff_mem, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, spanSingleton_mul_le_iff, mem_one_iff, mem_add, eq_spanSingleton_mul, mem_coeIdeal, mem_dual, mem_coeIdeal_of_mem, mem_spanSingleton, mem_zero_iff, mul_le, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, one_mem_inv_coe_ideal, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, coeToSet_coeToSubmodule, ext_iff, exists_ne_zero_mem_isInteger, zero_mem, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', NumberField.mem_span_basisOfFractionalIdeal, mem_singleton_mul, mem_spanSingleton_self, mem_coe, mem_canonicalEquiv_apply, Ideal.exist_integer_multiples_notMem, equivNum_apply, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, mem_extended_iff, den_mem_inv, mem_div_iff_of_ne_zero, mem_inv_iff, map_mem_map, exists_notMem_one_of_ne_bot, coe_extended_eq_span
|
instZero 📖 | CompOp | 38 mathmath: eq_zero_iff, divMod_zero_left, spanFinset_eq_zero, instMulPosStrictMonoNonZeroDivisors, eq_zero_or_one_of_isField, instMulPosReflectLENonZeroDivisors, le_zero_iff, zero_of_num_eq_bot, coeToSubmodule_eq_bot, extended_zero, num_zero_eq, extendedHomₐ_eq_zero_iff, isNoetherian_zero, bot_eq_zero, coeIdeal_eq_zero', map_eq_zero_iff, mem_zero_iff, dual_zero, spanSingleton_zero, coeIdeal_bot, divMod_zero_right, count_zero, spanSingleton_eq_zero_iff, div_zero, coeIdeal_eq_zero, dual_eq_zero_iff, instPosMulStrictMonoNonZeroDivisors, inv_zero', eq_zero_or_one, zero_le, count_mul', absNorm_eq_zero_iff, num_eq_zero_iff, zero_divMod, instPosMulReflectLENonZeroDivisors, extended_eq_zero_iff, coe_zero, map_zero
|
lattice 📖 | CompOp | — |
mul 📖 | CompOp | 2 mathmath: mul_eq_mul, mul_def'
|
num 📖 | CompOp | 11 mathmath: isUnit_num, num_zero_eq, num_le_mul_inv, absNorm_eq, den_mul_self_eq_num, absNorm_div_norm_eq_absNorm_div_norm, equivNum_apply, den_mul_self_eq_num', ClassGroup.integralRep_mem_nonZeroDivisors, num_eq_zero_iff, num_le
|
orderBot 📖 | CompOp | 3 mathmath: absNorm_bot, bot_eq_zero, bot_lt_mul_inv
|