Basic

📁 Source: Mathlib/NumberTheory/NumberField/Basic.lean

Statistics

Metric	Count
Definitions RingOfIntegers, algEquiv, basis, equiv, instAlgebra, instAlgebra_1, instCoeHead, instMulSemiringAction, mapAlgEquiv, mapAlgHom, mapRingEquiv, mapRingHom, restrict, restrict_addMonoidHom, restrict_monoidHom, val, instCommRingRingOfIntegers, instIsDomainRingOfIntegers, instNontrivialRingOfIntegers, inst_ringOfIntegersAlgebra, integralBasis, term𝓞, ringOfIntegersEquiv	23
Theorems instNumberFieldRat, not_isField, injective, coe_eq_algebraMap, coe_eq_zero_iff, coe_injective, coe_mk, coe_ne_zero_iff, eq_iff, ext, ext_iff, extension_algebra_isIntegral, extension_isNoetherian, instCharZero, instCharZero_1, instFG, instFreeInt, instIsDedekindDomain, instIsFractionRing, instIsIntegralClosure, instIsIntegralClosureInt, instIsIntegralInt, instIsIntegrallyClosed, instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, instIsNoetherianInt, instIsScalarTower, instIsScalarTower_1, instIsTorsionFree, instIsTorsionFree_1, instIsTorsionFree_2, instNeZeroIdealOfIsMaximal, instSMulDistribClass, inst_isScalarTower, isIntegral, isIntegral_coe, ker_algebraMap_eq_bot, mapRingEquiv_apply, mapRingEquiv_symm_apply, mapRingHom_apply, map_mk, minpoly_coe, mk_add_mk, mk_eq_mk, mk_mul_mk, mk_one, mk_sub_mk, mk_zero, neg_mk, not_isField, rank, instFiniteDimensional, integralBasis_apply, integralBasis_repr_apply, isAlgebraic, mem_span_integralBasis, of_intermediateField, of_module_finite, of_ringEquiv, of_subfield, of_tower, to_charZero, to_finiteDimensional, numberField, ringOfIntegersEquiv_apply_coe, ringOfIntegersEquiv_symm_apply_coe	65
Total	88

AdjoinRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNumberFieldRat 📖	mathematical	—	NumberField AdjoinRoot Rat.commRing instField Rat.instField	—	charZero_of_injective_algebraMap RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Rat.instCharZero PowerBasis.finite Irreducible.ne_zero Fact.out

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isField 📖	mathematical	—	IsField instSemiring	—	not_even_one Nat.instAtLeastTwoHAddOfNat two_mul IsField.mul_inv_cancel two_ne_zero

NumberField

Definitions

Name	Category	Theorems
RingOfIntegers 📖	CompOp	355 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one, Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', basisMatrix_eq_embeddingsMatrixReindex, mixedEmbedding.fundamentalCone.expMapBasis_apply', mixedEmbedding.fundamentalDomain_integerLattice, IsCyclotomicExtension.Rat.five_pid, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', Rat.RingOfIntegers.isUnit_iff, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow, RingOfIntegers.inst_isScalarTower, mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, canonicalEmbedding.mem_span_latticeBasis, integralBasis_apply, IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow, Units.logEmbedding_fundSystem, prod_nonarchAbsVal_eq, isCoprime_differentIdeal_of_isCoprime_discr, Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, FinitePlace.mk_apply, instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Units.fun_eq_repr, canonicalEmbedding.latticeBasis_apply, IsCMField.unitsComplexConj_torsion, hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', RingOfIntegers.instSMulDistribClass, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, RingOfIntegers.not_isField, mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, mixedEmbedding.norm_unit_smul, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, mixedEmbedding.mem_idealLattice, mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, Units.regOfFamily_eq_det, Units.dirichletUnitTheorem.seq_decreasing, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, Ideal.torsionMapQuot_apply, RingOfIntegers.instIsFractionRing, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, IsCyclotomicExtension.Rat.Three.coe_eta, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', RingOfIntegers.exponent_eq_sInf, Units.pos_at_place, RingOfIntegers.instIsTorsionFree_1, mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, RingOfIntegers.withValEquiv_symm_apply, Units.dirichletUnitTheorem.seq_next, Ideal.rootsOfUnityMapQuot_injective, Units.coe_mul, mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, FinitePlace.prod_eq_inv_abs_norm_int, mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integerSet, Units.dirichletUnitTheorem.logEmbedding_component_le, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, mixedEmbedding.exists_primitive_element_lt_of_isComplex, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, FinitePlace.norm_embedding_eq, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc, instIsGaloisGroupIntRingOfIntegersOfRat, mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Units.map_complexEmbedding_torsion, RingOfIntegers.instIsTorsionFree_2, Units.span_basisOfIsMaxRank, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, Units.logEmbeddingQuot_apply, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one, mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, canonicalEmbedding.integralBasis_repr_apply, Units.basisOfIsMaxRank_apply, RingOfIntegers.isUnit_norm_of_isGalois, Units.regulator_eq_det, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, RingOfIntegers.extension_algebra_isIntegral, mixedEmbedding.fundamentalDomain_idealLattice, mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, Units.coe_coe, Algebra.coe_norm_int, Units.instFiniteIntAdditiveUnitsRingOfIntegers, Units.finrank_mul_regOfFamily_eq_det, mixedEmbedding.mem_span_fractionalIdealLatticeBasis, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, det_basisOfFractionalIdeal_eq_absNorm, RingOfIntegers.coe_eq_zero_iff, Units.complexEmbedding_injective, RingOfIntegers.instIsNoetherianInt, Units.norm, RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two, RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, mixedEmbedding.span_idealLatticeBasis, IsPrimitiveRoot.integralPowerBasis'_gen, IsCMField.coe_ringOfIntegersComplexConj, Units.fundSystem_mk, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', FinitePlace.maximalIdeal_injective, IsCMField.indexRealUnits_mul_eq, Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, mixedEmbedding.unit_smul_eq_iff_mul_eq, mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, RingOfIntegers.norm_algebraMap, IsPrimitiveRoot.power_basis_int'_dim, mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, Units.rank_modTorsion, RingOfIntegers.ker_algebraMap_eq_bot, mixedEmbedding.mem_span_latticeBasis, Units.dirichletUnitTheorem.sum_logEmbedding_component, mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, IsPrimitiveRoot.finite_quotient_span_sub_one', house.exists_ne_zero_int_vec_house_le, IsPrimitiveRoot.finite_quotient_span_sub_one, mixedEmbedding.covolume_idealLattice, RingOfIntegers.instIsDedekindDomain, classNumber_eq_one_iff, IsCMField.unitsMulComplexConjInv_apply_torsion, Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet, RingOfIntegers.not_dvd_exponent_iff, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, mixedEmbedding.fundamentalCone.quotIntNorm_apply, Units.mem_torsion, FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, discr_eq_discr, mixedEmbedding.fundamentalCone.integerSetToAssociates_apply, Units.regOfFamily_div_regulator, mixedEmbedding.fundamentalCone.exists_unit_smul_mem, IsCyclotomicExtension.ring_of_integers', IsCyclotomicExtension.Rat.Three.eta_sq, Units.coe_neg_one, mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', IsCyclotomicExtension.ringOfIntegers, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, mixedEmbedding.logMap_eq_logEmbedding, RingOfIntegers.norm_norm, IsCMField.closure_realFundSystem_sup_torsion, Ideal.tendsto_norm_le_div_atTop₀, isFinitePlace_iff, sum_nonarchAbsVal_eq, Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, IsCyclotomicExtension.Rat.inertiaDeg_eq, Units.dirichletUnitTheorem.seq_norm_le, RingOfIntegers.rank, integralBasis_repr_apply, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Units.dirichletUnitTheorem.mult_log_place_eq_zero, Units.closure_fundSystem_sup_torsion_eq_top, FinitePlace.coe_apply, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', RingOfIntegers.isUnit_norm, FinitePlace.equivHeightOneSpectrum_symm_apply, Units.torsion_eq_one_or_neg_one_of_odd_finrank, mixedEmbedding.span_latticeBasis, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, RingOfIntegers.instIsTorsionFree, Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, Units.regOfFamily_div_regOfFamily, RingOfIntegers.withValEquiv_apply, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, mixedEmbedding.exists_ne_zero_mem_ideal_lt, RingOfIntegers.coe_injective, RingOfIntegers.instFreeInt, mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, IsCMField.unitsMulComplexConjInv_ker, RingOfIntegers.isIntegral_coe, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, IsCyclotomicExtension.Rat.Three.Units.mem, Units.complexEmbedding_apply, fractionalIdeal_rank, RingOfIntegers.instCharZero, mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, RingOfIntegers.mapRingHom_apply, RingOfIntegers.coe_norm, Units.coe_pow, mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one, IsCMField.unitsMulComplexConjInv_apply, Units.abs_det_eq_abs_det, mixedEmbedding.exists_primitive_element_lt_of_isReal, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, instIsGaloisGroupRingOfIntegersOfNumberField, HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le, inverse_basisMatrix_mulVec_eq_repr, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, RingOfIntegers.instIsIntegralClosureInt, IsCMField.ringOfIntegersComplexConj_eq_self_iff, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Units.coe_injective, mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, mixedEmbedding.logMap_unit_smul, Units.coe_one, IsCMField.mem_realUnits_iff, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, canonicalEmbedding.mem_rat_span_latticeBasis, mixedEmbedding.unitSMul_smul, RingOfIntegers.extension_isNoetherian, mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt, IsCMField.unitsComplexConj_eq_self_iff, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, exists_ideal_in_class_of_norm_le, IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, Rat.ringOfIntegersEquiv_apply_coe, Units.rootsOfUnity_eq_torsion, Ideal.tendsto_norm_le_div_atTop, mixedEmbedding.exists_ne_zero_mem_ideal_lt', IsCyclotomicExtension.Rat.inertiaDegIn_eq, Ideal.rootsOfUnityMapQuot_apply, RingOfIntegers.coe_eq_algebraMap, mem_span_integralBasis, RingOfIntegers.mapRingEquiv_apply, RingOfIntegers.neg_mk, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, IsCyclotomicExtension.Rat.three_pid, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, torsionOrder_dvd_absNorm_sub_one, Units.dirichletUnitTheorem.logEmbedding_component, Units.coe_zpow, mem_span_basisOfFractionalIdeal, exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, Units.logEmbeddingQuot_injective, mixedEmbedding.latticeBasis_apply, mixedEmbedding.unit_smul_eq_zero, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, Ideal.torsionMapQuot_injective, RingOfIntegers.exponent_eq_one_iff, IsPrimitiveRoot.idealQuotient_mk, RingOfIntegers.instIsIntegrallyClosed, mixedEmbedding.latticeBasis_repr_apply, RingOfIntegers.isIntegral, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow, IsPrimitiveRoot.integralPowerBasis_dim, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime, IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd, isUnit_iff_norm, mixedEmbedding.fractionalIdealLatticeBasis_apply, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, RingOfIntegers.instIsScalarTower, Units.instFGUnitsRingOfIntegers, Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, RingOfIntegers.instIsScalarTower_1, mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, RingOfIntegers.instIsIntegralInt, IsCMField.indexRealUnits_eq_two_iff, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one, Rat.ringOfIntegersEquiv_symm_apply_coe, IsCMField.RingOfIntegers.complexConj_eq_self_iff, IsPrimitiveRoot.integralPowerBasis_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq, mixedEmbedding.volume_fundamentalDomain_latticeBasis, Units.logEmbeddingEquiv_apply, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, Units.isMaxRank_iff_closure_finiteIndex, Units.exist_unique_eq_mul_prod, basisOfFractionalIdeal_apply, mixedEmbedding.logMap_torsion_smul, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Units.rootsOfUnity_eq_one, RingOfIntegers.algebraMap_norm_algebraMap, FinitePlace.isFinitePlace, instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Units.finiteIndex_iff_sup_torsion_finiteIndex, RingOfIntegers.instNeZeroIdealOfIsMaximal, RingOfIntegers.map_mk, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, mixedEmbedding.fundamentalCone.mem_idealSet, IsPrimitiveRoot.zeta_sub_one_prime, Ideal.tendsto_norm_le_and_mk_eq_div_atTop, mixedEmbedding.fundamentalCone.integerSetToAssociates_surjective, Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mixedEmbedding.fundamentalCone.idealSetEquiv_apply, canonicalEmbedding_eq_basisMatrix_mulVec, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, mixedEmbedding.fundamentalCone.mem_integerSet, coe_discr, Units.finrank_mul_regulator_eq_det, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul, instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, mixedEmbedding.disjoint_span_commMap_ker, Units.sum_mult_mul_log, Algebra.coe_trace_int, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, RingOfIntegers.coe_algebraMap_norm, Units.regulator_eq_det', RingOfIntegers.minpoly_coe, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, Units.dirichletUnitTheorem.logEmbedding_ker, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, Units.dirichletUnitTheorem.exists_unit, IsCMField.map_unitsMulComplexConjInv_torsion, Units.complexEmbedding_inj, RingOfIntegers.algebraMap.injective, RingOfIntegers.instIsIntegralClosure, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', mixedEmbedding.norm_unit, Units.regOfFamily_eq_det', IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime, RingOfIntegers.mapRingEquiv_symm_apply, IsCMField.complexConj_torsion, RingOfIntegers.instCharZero_1, RingOfIntegers.dvd_norm, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, house.basis_repr_norm_le_const_mul_house, IsCMField.Units.complexConj_eq_self_iff, mixedEmbedding.fundamentalCone.expMap_basis_of_ne, IsCMField.index_unitsMulComplexConjInv_range_dvd, Rat.ringOfIntegersWithValEquiv_apply, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mixedEmbedding.mem_rat_span_latticeBasis, IsPrimitiveRoot.toInteger_cube_eq_one, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, IsPrimitiveRoot.zeta_sub_one_prime', RingOfIntegers.instFG, mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one
instCommRingRingOfIntegers 📖	CompOp	346 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one, Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', basisMatrix_eq_embeddingsMatrixReindex, mixedEmbedding.fundamentalCone.expMapBasis_apply', mixedEmbedding.fundamentalDomain_integerLattice, IsCyclotomicExtension.Rat.five_pid, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', Rat.RingOfIntegers.isUnit_iff, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow, RingOfIntegers.inst_isScalarTower, mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, canonicalEmbedding.mem_span_latticeBasis, integralBasis_apply, IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow, Units.logEmbedding_fundSystem, prod_nonarchAbsVal_eq, isCoprime_differentIdeal_of_isCoprime_discr, Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, FinitePlace.mk_apply, instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Units.fun_eq_repr, canonicalEmbedding.latticeBasis_apply, IsCMField.unitsComplexConj_torsion, hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', RingOfIntegers.instSMulDistribClass, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, RingOfIntegers.not_isField, mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, mixedEmbedding.norm_unit_smul, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, mixedEmbedding.mem_idealLattice, mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, Units.regOfFamily_eq_det, Units.dirichletUnitTheorem.seq_decreasing, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, Ideal.torsionMapQuot_apply, RingOfIntegers.instIsFractionRing, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, IsCyclotomicExtension.Rat.Three.coe_eta, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', RingOfIntegers.exponent_eq_sInf, Units.pos_at_place, RingOfIntegers.instIsTorsionFree_1, mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, RingOfIntegers.withValEquiv_symm_apply, Ideal.rootsOfUnityMapQuot_injective, Units.coe_mul, mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, FinitePlace.prod_eq_inv_abs_norm_int, mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integerSet, Units.dirichletUnitTheorem.logEmbedding_component_le, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, FinitePlace.norm_embedding_eq, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc, instIsGaloisGroupIntRingOfIntegersOfRat, mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Units.map_complexEmbedding_torsion, RingOfIntegers.instIsTorsionFree_2, Units.span_basisOfIsMaxRank, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, Units.logEmbeddingQuot_apply, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one, canonicalEmbedding.integralBasis_repr_apply, Units.basisOfIsMaxRank_apply, RingOfIntegers.isUnit_norm_of_isGalois, Units.regulator_eq_det, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, RingOfIntegers.extension_algebra_isIntegral, mixedEmbedding.fundamentalDomain_idealLattice, mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, Units.coe_coe, Algebra.coe_norm_int, Units.instFiniteIntAdditiveUnitsRingOfIntegers, Units.finrank_mul_regOfFamily_eq_det, mixedEmbedding.mem_span_fractionalIdealLatticeBasis, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, det_basisOfFractionalIdeal_eq_absNorm, RingOfIntegers.coe_eq_zero_iff, Units.complexEmbedding_injective, RingOfIntegers.instIsNoetherianInt, Units.norm, RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two, RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, mixedEmbedding.span_idealLatticeBasis, IsPrimitiveRoot.integralPowerBasis'_gen, IsCMField.coe_ringOfIntegersComplexConj, Units.fundSystem_mk, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', FinitePlace.maximalIdeal_injective, IsCMField.indexRealUnits_mul_eq, Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, mixedEmbedding.unit_smul_eq_iff_mul_eq, mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, RingOfIntegers.norm_algebraMap, IsPrimitiveRoot.power_basis_int'_dim, mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, Units.rank_modTorsion, RingOfIntegers.ker_algebraMap_eq_bot, mixedEmbedding.mem_span_latticeBasis, Units.dirichletUnitTheorem.sum_logEmbedding_component, IsPrimitiveRoot.finite_quotient_span_sub_one', house.exists_ne_zero_int_vec_house_le, IsPrimitiveRoot.finite_quotient_span_sub_one, mixedEmbedding.covolume_idealLattice, RingOfIntegers.instIsDedekindDomain, classNumber_eq_one_iff, IsCMField.unitsMulComplexConjInv_apply_torsion, Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet, RingOfIntegers.not_dvd_exponent_iff, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, mixedEmbedding.fundamentalCone.quotIntNorm_apply, Units.mem_torsion, FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, discr_eq_discr, mixedEmbedding.fundamentalCone.integerSetToAssociates_apply, Units.regOfFamily_div_regulator, mixedEmbedding.fundamentalCone.exists_unit_smul_mem, IsCyclotomicExtension.ring_of_integers', IsCyclotomicExtension.Rat.Three.eta_sq, Units.coe_neg_one, IsCyclotomicExtension.ringOfIntegers, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, mixedEmbedding.logMap_eq_logEmbedding, RingOfIntegers.norm_norm, IsCMField.closure_realFundSystem_sup_torsion, Ideal.tendsto_norm_le_div_atTop₀, isFinitePlace_iff, sum_nonarchAbsVal_eq, Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, IsCyclotomicExtension.Rat.inertiaDeg_eq, Units.dirichletUnitTheorem.seq_norm_le, RingOfIntegers.rank, integralBasis_repr_apply, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Units.dirichletUnitTheorem.mult_log_place_eq_zero, Units.closure_fundSystem_sup_torsion_eq_top, FinitePlace.coe_apply, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', RingOfIntegers.isUnit_norm, FinitePlace.equivHeightOneSpectrum_symm_apply, Units.torsion_eq_one_or_neg_one_of_odd_finrank, mixedEmbedding.span_latticeBasis, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, RingOfIntegers.instIsTorsionFree, Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, Units.regOfFamily_div_regOfFamily, RingOfIntegers.withValEquiv_apply, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, mixedEmbedding.exists_ne_zero_mem_ideal_lt, RingOfIntegers.coe_injective, RingOfIntegers.instFreeInt, mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, IsCMField.unitsMulComplexConjInv_ker, RingOfIntegers.isIntegral_coe, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, IsCyclotomicExtension.Rat.Three.Units.mem, Units.complexEmbedding_apply, fractionalIdeal_rank, RingOfIntegers.instCharZero, mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, RingOfIntegers.mapRingHom_apply, RingOfIntegers.coe_norm, Units.coe_pow, mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one, IsCMField.unitsMulComplexConjInv_apply, Units.abs_det_eq_abs_det, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, instIsGaloisGroupRingOfIntegersOfNumberField, HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le, inverse_basisMatrix_mulVec_eq_repr, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, RingOfIntegers.instIsIntegralClosureInt, IsCMField.ringOfIntegersComplexConj_eq_self_iff, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Units.coe_injective, mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, mixedEmbedding.logMap_unit_smul, Units.coe_one, IsCMField.mem_realUnits_iff, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, canonicalEmbedding.mem_rat_span_latticeBasis, mixedEmbedding.unitSMul_smul, RingOfIntegers.extension_isNoetherian, IsCMField.unitsComplexConj_eq_self_iff, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, exists_ideal_in_class_of_norm_le, IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, Rat.ringOfIntegersEquiv_apply_coe, Units.rootsOfUnity_eq_torsion, Ideal.tendsto_norm_le_div_atTop, mixedEmbedding.exists_ne_zero_mem_ideal_lt', IsCyclotomicExtension.Rat.inertiaDegIn_eq, Ideal.rootsOfUnityMapQuot_apply, RingOfIntegers.coe_eq_algebraMap, mem_span_integralBasis, RingOfIntegers.mapRingEquiv_apply, RingOfIntegers.neg_mk, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, IsCyclotomicExtension.Rat.three_pid, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, torsionOrder_dvd_absNorm_sub_one, Units.dirichletUnitTheorem.logEmbedding_component, Units.coe_zpow, mem_span_basisOfFractionalIdeal, Units.logEmbeddingQuot_injective, mixedEmbedding.latticeBasis_apply, mixedEmbedding.unit_smul_eq_zero, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, Ideal.torsionMapQuot_injective, RingOfIntegers.exponent_eq_one_iff, IsPrimitiveRoot.idealQuotient_mk, RingOfIntegers.instIsIntegrallyClosed, mixedEmbedding.latticeBasis_repr_apply, RingOfIntegers.isIntegral, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow, IsPrimitiveRoot.integralPowerBasis_dim, RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime, IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd, isUnit_iff_norm, mixedEmbedding.fractionalIdealLatticeBasis_apply, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, RingOfIntegers.instIsScalarTower, Units.instFGUnitsRingOfIntegers, Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, RingOfIntegers.instIsScalarTower_1, mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, RingOfIntegers.instIsIntegralInt, IsCMField.indexRealUnits_eq_two_iff, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one, Rat.ringOfIntegersEquiv_symm_apply_coe, IsCMField.RingOfIntegers.complexConj_eq_self_iff, IsPrimitiveRoot.integralPowerBasis_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq, mixedEmbedding.volume_fundamentalDomain_latticeBasis, Units.logEmbeddingEquiv_apply, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, Units.isMaxRank_iff_closure_finiteIndex, Units.exist_unique_eq_mul_prod, basisOfFractionalIdeal_apply, mixedEmbedding.logMap_torsion_smul, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Units.rootsOfUnity_eq_one, RingOfIntegers.algebraMap_norm_algebraMap, FinitePlace.isFinitePlace, instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Units.finiteIndex_iff_sup_torsion_finiteIndex, RingOfIntegers.instNeZeroIdealOfIsMaximal, RingOfIntegers.map_mk, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, mixedEmbedding.fundamentalCone.mem_idealSet, IsPrimitiveRoot.zeta_sub_one_prime, Ideal.tendsto_norm_le_and_mk_eq_div_atTop, mixedEmbedding.fundamentalCone.integerSetToAssociates_surjective, Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mixedEmbedding.fundamentalCone.idealSetEquiv_apply, canonicalEmbedding_eq_basisMatrix_mulVec, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, coe_discr, Units.finrank_mul_regulator_eq_det, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul, instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, mixedEmbedding.disjoint_span_commMap_ker, Units.sum_mult_mul_log, Algebra.coe_trace_int, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, RingOfIntegers.coe_algebraMap_norm, Units.regulator_eq_det', RingOfIntegers.minpoly_coe, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, Units.dirichletUnitTheorem.logEmbedding_ker, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, Units.dirichletUnitTheorem.exists_unit, IsCMField.map_unitsMulComplexConjInv_torsion, Units.complexEmbedding_inj, RingOfIntegers.algebraMap.injective, RingOfIntegers.instIsIntegralClosure, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', mixedEmbedding.norm_unit, Units.regOfFamily_eq_det', IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime, RingOfIntegers.mapRingEquiv_symm_apply, IsCMField.complexConj_torsion, RingOfIntegers.instCharZero_1, RingOfIntegers.dvd_norm, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, house.basis_repr_norm_le_const_mul_house, IsCMField.Units.complexConj_eq_self_iff, mixedEmbedding.fundamentalCone.expMap_basis_of_ne, IsCMField.index_unitsMulComplexConjInv_range_dvd, Rat.ringOfIntegersWithValEquiv_apply, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mixedEmbedding.mem_rat_span_latticeBasis, IsPrimitiveRoot.toInteger_cube_eq_one, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, IsPrimitiveRoot.zeta_sub_one_prime', RingOfIntegers.instFG, mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one
instIsDomainRingOfIntegers 📖	CompOp	4 math math: isCoprime_differentIdeal_of_isCoprime_discr, exists_ideal_in_class_of_norm_le, Ideal.tendsto_norm_le_and_mk_eq_div_atTop, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply
instNontrivialRingOfIntegers 📖	CompOp	10 math math: mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Ideal.tendsto_norm_le_div_atTop₀, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, exists_ideal_in_class_of_norm_le, Ideal.tendsto_norm_le_div_atTop, torsionOrder_dvd_absNorm_sub_one, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Ideal.tendsto_norm_le_and_mk_eq_div_atTop
inst_ringOfIntegersAlgebra 📖	CompOp	16 math math: RingOfIntegers.inst_isScalarTower, isCoprime_differentIdeal_of_isCoprime_discr, RingOfIntegers.instIsTorsionFree_1, RingOfIntegers.extension_algebra_isIntegral, IsCMField.coe_ringOfIntegersComplexConj, RingOfIntegers.norm_algebraMap, RingOfIntegers.ker_algebraMap_eq_bot, instIsGaloisGroupRingOfIntegersOfNumberField, IsCMField.ringOfIntegersComplexConj_eq_self_iff, IsCMField.mem_realUnits_iff, RingOfIntegers.extension_isNoetherian, RingOfIntegers.instIsScalarTower_1, RingOfIntegers.algebraMap_norm_algebraMap, RingOfIntegers.coe_algebraMap_norm, RingOfIntegers.algebraMap.injective, RingOfIntegers.dvd_norm
integralBasis 📖	CompOp	13 math math: basisMatrix_eq_embeddingsMatrixReindex, integralBasis_apply, canonicalEmbedding.latticeBasis_apply, canonicalEmbedding.integralBasis_repr_apply, det_basisOfFractionalIdeal_eq_absNorm, integralBasis_repr_apply, inverse_basisMatrix_mulVec_eq_repr, mem_span_integralBasis, mixedEmbedding.latticeBasis_apply, mixedEmbedding.latticeBasis_repr_apply, canonicalEmbedding_eq_basisMatrix_mulVec, coe_discr, house.basis_repr_norm_le_const_mul_house
term𝓞 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteDimensional 📖	mathematical	—	FiniteDimensional Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Module.Finite.of_restrictScalars_finite to_charZero IsScalarTower.rat to_finiteDimensional
integralBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Module.Free.ChooseBasisIndex RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingRingOfIntegers AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing RingOfIntegers.instFreeInt Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero Module.Basis.instFunLike integralBasis RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingOfIntegers.instAlgebra_1 RingOfIntegers.basis	—	RingOfIntegers.instFreeInt Module.Basis.localizationLocalization_apply Rat.isFractionRing to_charZero AddCommGroup.intIsScalarTower RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors
integralBasis_repr_apply 📖	mathematical	—	DFunLike.coe Finsupp Module.Free.ChooseBasisIndex RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingRingOfIntegers AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing RingOfIntegers.instFreeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Rat.semiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids EuclideanDomain.toCommRing Field.toEuclideanDomain Finsupp.instAddCommMonoid Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr integralBasis RingHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingOfIntegers.instAlgebra_1 Int.instCommSemiring Ring.toIntAlgebra DivisionRing.toRing Rat.instDivisionRing RingOfIntegers.basis	—	RingOfIntegers.instFreeInt Module.Basis.localizationLocalization_repr_algebraMap Rat.isFractionRing to_charZero AddCommGroup.intIsScalarTower RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors
isAlgebraic 📖	mathematical	—	Algebra.IsAlgebraic Rat.commRing DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatAlgebra to_charZero	—	Algebra.IsAlgebraic.of_finite Rat.nontrivial to_charZero to_finiteDimensional
mem_span_integralBasis 📖	mathematical	—	Submodule Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toIntModule Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Free.ChooseBasisIndex RingOfIntegers instCommRingRingOfIntegers CommRing.toRing RingOfIntegers.instFreeInt DFunLike.coe Module.Basis Rat.semiring Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra to_charZero Module.Basis.instFunLike integralBasis Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Subring.instSetLike RingHom.range algebraMap CommRing.toCommSemiring RingOfIntegers.instAlgebra_1	—	RingOfIntegers.instFreeInt to_charZero RingHomSurjective.ids NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Module.Basis.localizationLocalization_span Rat.isFractionRing RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors
of_intermediateField 📖	mathematical	—	NumberField IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField	—	of_module_finite IsScalarTower.left IntermediateField.finiteDimensional_left instFiniteDimensional
of_module_finite 📖	mathematical	—	NumberField	—	charZero_of_injective_algebraMap RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing to_charZero Module.Finite.trans IsScalarTower.rat to_finiteDimensional
of_ringEquiv 📖	mathematical	—	NumberField	—	CharZero.of_addMonoidHom to_charZero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.injective LinearEquiv.finiteDimensional RingHomInvPair.ids RingEquivClass.toLinearEquivClassRat to_finiteDimensional
of_subfield 📖	mathematical	—	NumberField Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike Subfield.toField	—	SubsemiringClass.instCharZero SubfieldClass.toSubringClass Subfield.instSubfieldClass to_charZero FiniteDimensional.left instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain Rat.isDomain EuclideanDomain.to_principal_ideal_domain to_finiteDimensional IsScalarTower.rat IsLocalRing.toNontrivial Field.instIsLocalRing
of_tower 📖	mathematical	—	NumberField	—	of_module_finite Module.Finite.left instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instFiniteDimensional IsLocalRing.toNontrivial Field.instIsLocalRing
to_charZero 📖	mathematical	—	CharZero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	—
to_finiteDimensional 📖	mathematical	—	FiniteDimensional Rat.instDivisionRing Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra to_charZero	—	—

NumberField.RingOfIntegers

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	—
basis 📖	CompOp	2 math math: NumberField.integralBasis_apply, NumberField.integralBasis_repr_apply
equiv 📖	CompOp	—
instAlgebra 📖	CompOp	6 math math: instIsTorsionFree_2, instIsScalarTower, instIsScalarTower_1, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, instIsIntegralClosure, NumberField.IsCMField.Units.complexConj_eq_self_iff
instAlgebra_1 📖	CompOp	90 math math: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.canonicalEmbedding.mem_span_latticeBasis, NumberField.integralBasis_apply, NumberField.prod_nonarchAbsVal_eq, NumberField.FinitePlace.mk_apply, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, instSMulDistribClass, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.Units.regOfFamily_eq_det, NumberField.Units.dirichletUnitTheorem.seq_decreasing, instIsFractionRing, NumberField.Units.pos_at_place, withValEquiv_symm_apply, NumberField.Units.coe_mul, NumberField.FinitePlace.norm_embedding_eq, Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, NumberField.Units.regulator_eq_det, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.Units.coe_coe, NumberField.Units.finrank_mul_regOfFamily_eq_det, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, NumberField.det_basisOfFractionalIdeal_eq_absNorm, coe_eq_zero_iff, NumberField.Units.norm, instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.Units.mem_torsion, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, NumberField.Units.coe_neg_one, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.isFinitePlace_iff, NumberField.sum_nonarchAbsVal_eq, NumberField.integralBasis_repr_apply, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, NumberField.FinitePlace.coe_apply, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, instIsTorsionFree, withValEquiv_apply, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, coe_injective, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, isIntegral_coe, NumberField.Units.complexEmbedding_apply, NumberField.fractionalIdeal_rank, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, NumberField.Units.coe_pow, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.Units.abs_det_eq_abs_det, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, NumberField.inverse_basisMatrix_mulVec_eq_repr, instIsIntegralClosureInt, NumberField.Units.coe_injective, NumberField.Units.coe_one, NumberField.mixedEmbedding.unitSMul_smul, Rat.ringOfIntegersEquiv_apply_coe, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', coe_eq_algebraMap, NumberField.mem_span_integralBasis, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, NumberField.Units.coe_zpow, NumberField.mem_span_basisOfFractionalIdeal, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, instIsScalarTower, instIsScalarTower_1, NumberField.basisOfFractionalIdeal_apply, RingOfIntegers.algebraMap_norm_algebraMap, NumberField.FinitePlace.isFinitePlace, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, map_mk, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.Units.finrank_mul_regulator_eq_det, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, NumberField.Units.sum_mult_mul_log, NumberField.Units.dirichletUnitTheorem.exists_unit, instIsIntegralClosure, NumberField.mixedEmbedding.norm_unit, NumberField.IsCMField.complexConj_torsion, NumberField.house.basis_repr_norm_le_const_mul_house, NumberField.IsCMField.Units.complexConj_eq_self_iff, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Rat.ringOfIntegersWithValEquiv_apply
instCoeHead 📖	CompOp	—
instMulSemiringAction 📖	CompOp	5 math math: instSMulDistribClass, instIsGaloisGroupIntRingOfIntegersOfRat, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, instIsGaloisGroupRingOfIntegersOfNumberField, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq
mapAlgEquiv 📖	CompOp	—
mapAlgHom 📖	CompOp	—
mapRingEquiv 📖	CompOp	2 math math: mapRingEquiv_apply, mapRingEquiv_symm_apply
mapRingHom 📖	CompOp	1 math math: mapRingHom_apply
restrict 📖	CompOp	—
restrict_addMonoidHom 📖	CompOp	—
restrict_monoidHom 📖	CompOp	—
val 📖	CompOp	40 math math: NumberField.FinitePlace.hasFiniteMulSupport_int, Rat.RingOfIntegers.isUnit_iff, NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, NumberField.adjoin_eq_top_of_infinitePlace_lt, NumberField.Units.dirichletUnitTheorem.seq_next, NumberField.FinitePlace.prod_eq_inv_abs_norm_int, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, NumberField.exists_conjugate_one_le_norm, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, NumberField.Units.coe_coe, Algebra.coe_norm_int, NumberField.IsCMField.coe_ringOfIntegersComplexConj, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt', NumberField.is_primitive_element_of_infinitePlace_lt, NumberField.FinitePlace.mulSupport_finite_int, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, mapRingHom_apply, RingOfIntegers.coe_norm, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, NumberField.inverse_basisMatrix_mulVec_eq_repr, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt, coe_eq_algebraMap, mapRingEquiv_apply, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd, NumberField.isUnit_iff_norm, ext_iff, Rat.ringOfIntegersEquiv_symm_apply_coe, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.InfinitePlace.one_le_of_lt_one, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, Algebra.coe_trace_int, RingOfIntegers.coe_algebraMap_norm, minpoly_coe, eq_iff, mapRingEquiv_symm_apply, NumberField.house.basis_repr_norm_le_const_mul_house

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_algebraMap 📖	mathematical	—	val DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1	—	—
coe_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coe_injective
coe_injective 📖	mathematical	—	NumberField.RingOfIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1	—	FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFree
coe_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	—	—
coe_ne_zero_iff 📖	—	—	—	—	map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coe_injective
eq_iff 📖	mathematical	—	val	—	ext_iff
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext
extension_algebra_isIntegral 📖	mathematical	—	Algebra.IsIntegral NumberField.RingOfIntegers NumberField.instCommRingRingOfIntegers CommRing.toRing NumberField.inst_ringOfIntegersAlgebra	—	IsIntegralClosure.isIntegral_algebra instIsIntegralClosure instIsScalarTower_1
extension_isNoetherian 📖	mathematical	—	IsNoetherian NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule NumberField.inst_ringOfIntegersAlgebra	—	IsIntegralClosure.isNoetherian instIsFractionRing instIsScalarTower instIsIntegralClosure instIsScalarTower_1 NumberField.instFiniteDimensional Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing PerfectField.ofCharZero NumberField.to_charZero instIsIntegrallyClosed IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing instIsDedekindDomain
instCharZero 📖	mathematical	—	CharZero NumberField.RingOfIntegers AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NumberField.instCommRingRingOfIntegers	—	—
instCharZero_1 📖	mathematical	—	CharZero NumberField.RingOfIntegers AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NumberField.instCommRingRingOfIntegers	—	CharZero.of_module
instFG 📖	mathematical	—	AddGroup.FG NumberField.RingOfIntegers AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing NumberField.instCommRingRingOfIntegers	—	Module.Finite.iff_addGroup_fg Module.IsNoetherian.finite instIsNoetherianInt
instFreeInt 📖	mathematical	—	Module.Free NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing	—	IsIntegralClosure.module_free Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower instIsIntegralClosureInt NumberField.to_finiteDimensional Int.instIsDomain Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain EuclideanDomain.to_principal_ideal_domain
instIsDedekindDomain 📖	mathematical	—	IsDedekindDomain NumberField.RingOfIntegers NumberField.instCommRingRingOfIntegers	—	IsIntegralClosure.isDedekindDomain Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower instIsIntegralClosureInt NumberField.to_finiteDimensional Int.instIsDomain Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain
instIsFractionRing 📖	mathematical	—	IsFractionRing NumberField.RingOfIntegers CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers Semifield.toCommSemiring Field.toSemifield instAlgebra_1	—	integralClosure.isFractionRing_of_finite_extension Rat.isFractionRing Int.instIsDomain NumberField.to_charZero AddCommGroup.intIsScalarTower NumberField.to_finiteDimensional
instIsIntegralClosure 📖	mathematical	—	IsIntegralClosure NumberField.RingOfIntegers NumberField.instCommRingRingOfIntegers CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instAlgebra DivisionRing.toRing Field.toDivisionRing instAlgebra_1	—	IsIntegralClosure.tower_top AddCommGroup.intIsScalarTower instIsIntegralClosureInt instIsIntegralInt
instIsIntegralClosureInt 📖	mathematical	—	IsIntegralClosure NumberField.RingOfIntegers Int.instCommRing CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing instAlgebra_1	—	integralClosure.isIntegralClosure
instIsIntegralInt 📖	mathematical	—	Algebra.IsIntegral NumberField.RingOfIntegers Int.instCommRing CommRing.toRing NumberField.instCommRingRingOfIntegers Ring.toIntAlgebra	—	IsIntegralClosure.isIntegral_algebra instIsIntegralClosureInt AddCommGroup.intIsScalarTower
instIsIntegrallyClosed 📖	mathematical	—	IsIntegrallyClosed NumberField.RingOfIntegers NumberField.instCommRingRingOfIntegers	—	integralClosure.isIntegrallyClosedOfFiniteExtension Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower Int.instIsDomain NumberField.to_finiteDimensional
instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors 📖	mathematical	—	IsLocalization NumberField.RingOfIntegers CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers Algebra.algebraMapSubmonoid Int.instCommSemiring CommSemiring.toSemiring Ring.toIntAlgebra CommRing.toRing nonZeroDivisors Semiring.toMonoidWithZero Int.instSemiring Semifield.toCommSemiring Field.toSemifield instAlgebra_1	—	IsIntegralClosure.isLocalization_of_isSeparable Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower instIsIntegralClosureInt Int.instIsDomain Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial NumberField.to_finiteDimensional PerfectField.ofCharZero Rat.instCharZero
instIsNoetherianInt 📖	mathematical	—	IsNoetherian NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing	—	IsIntegralClosure.isNoetherian Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower instIsIntegralClosureInt NumberField.to_finiteDimensional Int.instIsDomain Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain IsDedekindRing.toIsNoetherian
instIsScalarTower 📖	mathematical	—	IsScalarTower NumberField.RingOfIntegers Algebra.toSMul CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra_1 Semifield.toCommSemiring Ring.toSemiring instAlgebra	—	—
instIsScalarTower_1 📖	mathematical	—	IsScalarTower NumberField.RingOfIntegers Algebra.toSMul CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra_1 Ring.toSemiring DivisionRing.toRing Field.toDivisionRing instAlgebra	—	IsScalarTower.of_algebraMap_eq'
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra_1	—	—
instIsTorsionFree_1 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule NumberField.inst_ringOfIntegersAlgebra	—	Module.isTorsionFree_iff_algebraMap_injective algebraMap.injective
instIsTorsionFree_2 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra DivisionRing.toRing Field.toDivisionRing	—	Module.IsTorsionFree.trans_faithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instIsTorsionFree_1 instIsTorsionFree instIsScalarTower_1
instNeZeroIdealOfIsMaximal 📖	mathematical	—	Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ring.ne_bot_of_isMaximal_of_not_isField not_isField
instSMulDistribClass 📖	mathematical	—	SMulDistribClass NumberField.RingOfIntegers SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NumberField.instCommRingRingOfIntegers DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring instMulSemiringAction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivisionSemiring.toSemiring Algebra.toSMul CommRing.toCommSemiring instAlgebra_1	—	—
inst_isScalarTower 📖	mathematical	—	IsScalarTower NumberField.RingOfIntegers Algebra.toSMul CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra	—	IsScalarTower.of_algHom AlgHom.algHomClass
isIntegral 📖	mathematical	—	IsIntegral NumberField.RingOfIntegers Int.instCommRing CommRing.toRing NumberField.instCommRingRingOfIntegers Ring.toIntAlgebra	—	isIntegral_coe coe_eq_zero_iff Polynomial.hom_eval₂ IsScalarTower.algebraMap_eq AddCommGroup.intIsScalarTower
isIntegral_coe 📖	mathematical	—	IsIntegral Int.instCommRing DivisionRing.toRing Field.toDivisionRing Ring.toIntAlgebra DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1	—	—
ker_algebraMap_eq_bot 📖	mathematical	—	RingHom.ker NumberField.RingOfIntegers RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers RingHom.instFunLike RingHom.instRingHomClass algebraMap NumberField.inst_ringOfIntegersAlgebra Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	RingHom.instRingHomClass RingHom.ker_eq_bot_iff_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass IsLocalRing.toNontrivial Field.instIsLocalRing
mapRingEquiv_apply 📖	mathematical	—	val DFunLike.coe RingEquiv NumberField.RingOfIntegers Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike mapRingEquiv EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—
mapRingEquiv_symm_apply 📖	mathematical	—	val DFunLike.coe RingEquiv NumberField.RingOfIntegers Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm mapRingEquiv EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—
mapRingHom_apply 📖	mathematical	—	val DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers RingHom.instFunLike mapRingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
map_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 Subalgebra Int.instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	—	—
minpoly_coe 📖	mathematical	—	minpoly Int.instCommRing DivisionRing.toRing Field.toDivisionRing Ring.toIntAlgebra val NumberField.RingOfIntegers CommRing.toRing NumberField.instCommRingRingOfIntegers	—	minpoly.algebraMap_eq AddCommGroup.intIsScalarTower coe_injective
mk_add_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass	—	—
mk_eq_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	—	—
mk_mul_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing MulMemClass.mul_mem SubmonoidClass.toMulMemClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass	—	—
mk_one 📖	mathematical	—	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass OneMemClass.one DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass
mk_sub_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure AddSubgroupClass.sub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubringClass.addSubgroupClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Subalgebra.instSubringClass SubNegMonoid.toSub sub_mem	—	SubringClass.addSubgroupClass Subalgebra.instSubringClass
mk_zero 📖	mathematical	—	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass ZeroMemClass.zero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass
neg_mk 📖	mathematical	Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure	NumberField.RingOfIntegers NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing NumberField.instCommRingRingOfIntegers Subalgebra CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subalgebra.instSetLike integralClosure NegMemClass.neg_mem SubringClass.toNegMemClass Ring.toNonAssocRing Ring.toSemiring Subalgebra.instSubringClass	—	—
not_isField 📖	mathematical	—	IsField NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers	—	RingHom.injective_int instCharZero_1 NumberField.to_charZero Int.not_isField Algebra.IsIntegral.isField_iff_isField IsIntegralClosure.isIntegral_algebra instIsIntegralClosureInt AddCommGroup.intIsScalarTower
rank 📖	mathematical	—	Module.finrank NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing Rat.semiring EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	IsIntegralClosure.rank Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower instIsIntegralClosureInt NumberField.to_finiteDimensional Int.instIsDomain Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero instIsDomain

NumberField.RingOfIntegers.algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	mathematical	—	NumberField.RingOfIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers RingHom.instFunLike algebraMap NumberField.inst_ringOfIntegersAlgebra	—	RingHom.instRingHomClass RingHom.injective_iff_ker_eq_bot NumberField.RingOfIntegers.ker_algebraMap_eq_bot

Rat

Definitions

Name	Category	Theorems
ringOfIntegersEquiv 📖	CompOp	3 math math: IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, ringOfIntegersEquiv_apply_coe, ringOfIntegersEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
numberField 📖	mathematical	—	NumberField instField	—	instCharZero Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
ringOfIntegersEquiv_apply_coe 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.RingOfIntegers instField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringOfIntegersEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring semiring RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1	—	RingEquiv.surjective eq_intCast RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_intCast RingHom.instRingHomClass
ringOfIntegersEquiv_symm_apply_coe 📖	mathematical	—	NumberField.RingOfIntegers.val instField DFunLike.coe RingEquiv NumberField.RingOfIntegers Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.instCommRingRingOfIntegers Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringOfIntegersEquiv	—	eq_intCast RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass

---

← Back to Index