Basic

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

Statistics

Metric	Count
Definitions RingOfIntegers, algEquiv, basis, equiv, instAlgebra, instAlgebra_1, instCoeHead, instCommRing, instMulSemiringAction, mapAlgEquiv, mapAlgHom, mapRingEquiv, mapRingHom, restrict, restrict_addMonoidHom, restrict_monoidHom, val, inst_ringOfIntegersAlgebra, integralBasis, term𝓞, ringOfIntegersEquiv	21
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, instFreeInt, instIsDedekindDomain, instIsDomain, instIsFractionRing, instIsIntegralClosure, instIsIntegralClosureInt, instIsIntegralInt, instIsIntegrallyClosed, instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, instIsNoetherianInt, instIsScalarTower, instIsScalarTower_1, instIsTorsionFree, instIsTorsionFree_1, instIsTorsionFree_2, instNontrivial, 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	86

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	347 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, canonicalEmbedding.latticeBasis_apply, IsCMField.unitsComplexConj_torsion, RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b, Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', RingOfIntegers.instSMulDistribClass, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, RingOfIntegers.not_isField, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b, mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, mixedEmbedding.norm_unit_smul, FinitePlace.norm_def', IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, mixedEmbedding.mem_idealLattice, mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, Units.regOfFamily_eq_det, FinitePlace.embedding_apply, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, 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, FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube, mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, FermatLastTheoremForThreeGen.Solution'.H, RingOfIntegers.withValEquiv_symm_apply, FermatLastTheoremForThreeGen.Solution.hab, Units.coe_mul, FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b, mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, FinitePlace.prod_eq_inv_abs_norm_int, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, FinitePlace.norm_embedding_eq, RingOfIntegers.instIsDedekindDomainWithVal, 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, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, instIsGaloisGroupIntRingOfIntegersOfRat, mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, Units.map_complexEmbedding_torsion, RingOfIntegers.instIsTorsionFree_2, Units.span_basisOfIsMaxRank, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, Units.logEmbeddingQuot_apply, 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, FinitePlace.norm_lt_one_iff_mem, 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, FermatLastTheoremForThreeGen.Solution'.ha, IsPrimitiveRoot.finite_quotient_span_sub_one', RingOfIntegers.instNontrivial, IsPrimitiveRoot.finite_quotient_span_sub_one, mixedEmbedding.covolume_idealLattice, FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one, RingOfIntegers.instIsDedekindDomain, classNumber_eq_one_iff, IsCMField.unitsMulComplexConjInv_apply_torsion, Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, RingOfIntegers.not_dvd_exponent_iff, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, mixedEmbedding.fundamentalCone.quotIntNorm_apply, Units.mem_torsion, 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, Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, IsCyclotomicExtension.Rat.inertiaDeg_eq, RingOfIntegers.rank, integralBasis_repr_apply, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, RingOfIntegers.HeightOneSpectrum.adicAbv_def, 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, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', RingOfIntegers.isUnit_norm, Units.torsion_eq_one_or_neg_one_of_odd_finrank, mixedEmbedding.span_latticeBasis, FinitePlace.norm_def_int, 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, RingOfIntegers.withValEquiv_apply, 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.instIsDomain, 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, FermatLastTheoremForThreeGen.Solution'.hcdvd, 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', FermatLastTheoremForThreeGen.Solution'.hb, 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, 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, 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, RingOfIntegers.exponent_eq_one_iff, FinitePlace.norm_eq_one_iff_notMem, 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, IsCyclotomicExtension.Rat.ramificationIdx_of_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, toNNReal_valued_eq_adicAbv, mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, RingOfIntegers.instIsIntegralInt, FermatLastTheoremForThreeGen.Solution'.coprime, IsCMField.indexRealUnits_eq_two_iff, 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, 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.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, FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul, Units.finrank_mul_regulator_eq_det, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul, instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, mixedEmbedding.disjoint_span_commMap_ker, FinitePlace.norm_le_one, Units.sum_mult_mul_log, Algebra.coe_trace_int, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, FermatLastTheoremForThreeGen.lambda_sq_dvd_c, RingOfIntegers.coe_algebraMap_norm, Units.regulator_eq_det', RingOfIntegers.minpoly_coe, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b, Units.dirichletUnitTheorem.logEmbedding_ker, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, 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, FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite, IsCMField.complexConj_torsion, RingOfIntegers.instCharZero_1, FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd, RingOfIntegers.dvd_norm, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b, 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, FinitePlace.norm_def, 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, IsPrimitiveRoot.zeta_sub_one_prime', 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, FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd
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 RingOfIntegers.instCommRing 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 DivisionRing.toRing Algebra.id Semifield.toCommSemiring 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 RingOfIntegers.instCommRing 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 DivisionRing.toRing Algebra.id Semifield.toCommSemiring Int.instCommSemiring Ring.toIntAlgebra 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 RingOfIntegers.instCommRing 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 Subring.instSetLike RingHom.range algebraMap CommRing.toCommSemiring RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring	—	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 SubringClass.toSubsemiringClass 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	1 math math: instIsTorsionFree
instAlgebra_1 📖	CompOp	97 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.FinitePlace.norm_def', NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.Units.regOfFamily_eq_det, NumberField.FinitePlace.embedding_apply, 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, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, instIsTorsionFree_2, 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.FinitePlace.norm_lt_one_iff_mem, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.Units.mem_torsion, NumberField.Units.coe_neg_one, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.isFinitePlace_iff, NumberField.integralBasis_repr_apply, HeightOneSpectrum.adicAbv_def, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, NumberField.FinitePlace.coe_apply, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, NumberField.FinitePlace.norm_def_int, 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.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.FinitePlace.norm_eq_one_iff_notMem, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, instIsScalarTower, instIsScalarTower_1, NumberField.toNNReal_valued_eq_adicAbv, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, 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, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, NumberField.FinitePlace.norm_le_one, 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, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply
instCoeHead 📖	CompOp	—
instCommRing 📖	CompOp	345 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', NumberField.basisMatrix_eq_embeddingsMatrixReindex, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.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, inst_isScalarTower, NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet_mixedEmbedding, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, NumberField.canonicalEmbedding.mem_span_latticeBasis, NumberField.integralBasis_apply, IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow, NumberField.Units.logEmbedding_fundSystem, NumberField.prod_nonarchAbsVal_eq, NumberField.isCoprime_differentIdeal_of_isCoprime_discr, NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, NumberField.FinitePlace.mk_apply, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.IsCMField.unitsComplexConj_torsion, HeightOneSpectrum.one_lt_absNorm_nnreal, NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', instSMulDistribClass, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, not_isField, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, NumberField.mixedEmbedding.norm_unit_smul, NumberField.FinitePlace.norm_def', IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.Units.regOfFamily_eq_det, NumberField.FinitePlace.embedding_apply, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, 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, NumberField.Units.pos_at_place, instIsTorsionFree_1, FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, FermatLastTheoremForThreeGen.Solution'.H, withValEquiv_symm_apply, FermatLastTheoremForThreeGen.Solution.hab, NumberField.Units.coe_mul, FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, NumberField.FinitePlace.prod_eq_inv_abs_norm_int, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, NumberField.FinitePlace.norm_embedding_eq, instIsDedekindDomainWithVal, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, instIsGaloisGroupIntRingOfIntegersOfRat, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, NumberField.Units.map_complexEmbedding_torsion, instIsTorsionFree_2, NumberField.Units.span_basisOfIsMaxRank, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, NumberField.Units.logEmbeddingQuot_apply, NumberField.canonicalEmbedding.integralBasis_repr_apply, NumberField.Units.basisOfIsMaxRank_apply, RingOfIntegers.isUnit_norm_of_isGalois, NumberField.Units.regulator_eq_det, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, extension_algebra_isIntegral, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, NumberField.Units.coe_coe, Algebra.coe_norm_int, NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers, 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.complexEmbedding_injective, instIsNoetherianInt, NumberField.Units.norm, RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two, instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, NumberField.mixedEmbedding.span_idealLatticeBasis, IsPrimitiveRoot.integralPowerBasis'_gen, NumberField.IsCMField.coe_ringOfIntegersComplexConj, NumberField.Units.fundSystem_mk, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', NumberField.FinitePlace.maximalIdeal_injective, NumberField.IsCMField.indexRealUnits_mul_eq, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, NumberField.FinitePlace.norm_lt_one_iff_mem, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, RingOfIntegers.norm_algebraMap, IsPrimitiveRoot.power_basis_int'_dim, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, NumberField.Units.rank_modTorsion, ker_algebraMap_eq_bot, NumberField.mixedEmbedding.mem_span_latticeBasis, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, FermatLastTheoremForThreeGen.Solution'.ha, IsPrimitiveRoot.finite_quotient_span_sub_one', IsPrimitiveRoot.finite_quotient_span_sub_one, NumberField.mixedEmbedding.covolume_idealLattice, FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one, instIsDedekindDomain, NumberField.classNumber_eq_one_iff, NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion, NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, RingOfIntegers.not_dvd_exponent_iff, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply, NumberField.Units.mem_torsion, NumberField.discr_eq_discr, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_apply, NumberField.Units.regOfFamily_div_regulator, NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem, IsCyclotomicExtension.ring_of_integers', IsCyclotomicExtension.Rat.Three.eta_sq, NumberField.Units.coe_neg_one, IsCyclotomicExtension.ringOfIntegers, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, RingOfIntegers.norm_norm, NumberField.IsCMField.closure_realFundSystem_sup_torsion, NumberField.Ideal.tendsto_norm_le_div_atTop₀, NumberField.isFinitePlace_iff, NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, IsCyclotomicExtension.Rat.inertiaDeg_eq, rank, NumberField.integralBasis_repr_apply, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, HeightOneSpectrum.adicAbv_def, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, NumberField.FinitePlace.coe_apply, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', RingOfIntegers.isUnit_norm, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, NumberField.mixedEmbedding.span_latticeBasis, NumberField.FinitePlace.norm_def_int, instIsTorsionFree, NumberField.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, withValEquiv_apply, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, coe_injective, instFreeInt, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, NumberField.IsCMField.unitsMulComplexConjInv_ker, instIsDomain, isIntegral_coe, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, IsCyclotomicExtension.Rat.Three.Units.mem, NumberField.Units.complexEmbedding_apply, NumberField.fractionalIdeal_rank, instCharZero, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, mapRingHom_apply, RingOfIntegers.coe_norm, NumberField.Units.coe_pow, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one, NumberField.IsCMField.unitsMulComplexConjInv_apply, NumberField.Units.abs_det_eq_abs_det, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, instIsGaloisGroupRingOfIntegersOfNumberField, FermatLastTheoremForThreeGen.Solution'.hcdvd, NumberField.inverse_basisMatrix_mulVec_eq_repr, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, instIsIntegralClosureInt, NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, NumberField.Units.coe_injective, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, NumberField.mixedEmbedding.logMap_unit_smul, NumberField.Units.coe_one, NumberField.IsCMField.mem_realUnits_iff, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, NumberField.mixedEmbedding.unitSMul_smul, extension_isNoetherian, NumberField.IsCMField.unitsComplexConj_eq_self_iff, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', FermatLastTheoremForThreeGen.Solution'.hb, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, NumberField.exists_ideal_in_class_of_norm_le, IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, Rat.ringOfIntegersEquiv_apply_coe, NumberField.Units.rootsOfUnity_eq_torsion, NumberField.Ideal.tendsto_norm_le_div_atTop, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', IsCyclotomicExtension.Rat.inertiaDegIn_eq, coe_eq_algebraMap, NumberField.mem_span_integralBasis, mapRingEquiv_apply, neg_mk, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, IsCyclotomicExtension.Rat.three_pid, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, NumberField.Units.coe_zpow, NumberField.mem_span_basisOfFractionalIdeal, NumberField.Units.logEmbeddingQuot_injective, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.unit_smul_eq_zero, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, RingOfIntegers.exponent_eq_one_iff, NumberField.FinitePlace.norm_eq_one_iff_notMem, instIsIntegrallyClosed, NumberField.mixedEmbedding.latticeBasis_repr_apply, 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, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, NumberField.isUnit_iff_norm, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, instIsScalarTower, NumberField.Units.instFGUnitsRingOfIntegers, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, instIsScalarTower_1, NumberField.toNNReal_valued_eq_adicAbv, NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, instIsIntegralInt, FermatLastTheoremForThreeGen.Solution'.coprime, NumberField.IsCMField.indexRealUnits_eq_two_iff, Rat.ringOfIntegersEquiv_symm_apply_coe, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, IsPrimitiveRoot.integralPowerBasis_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.Units.logEmbeddingEquiv_apply, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, NumberField.Units.isMaxRank_iff_closure_finiteIndex, NumberField.Units.exist_unique_eq_mul_prod, NumberField.basisOfFractionalIdeal_apply, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, NumberField.Units.rootsOfUnity_eq_one, RingOfIntegers.algebraMap_norm_algebraMap, NumberField.FinitePlace.isFinitePlace, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, map_mk, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, IsPrimitiveRoot.zeta_sub_one_prime, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_surjective, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, NumberField.coe_discr, FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul, NumberField.Units.finrank_mul_regulator_eq_det, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, NumberField.mixedEmbedding.disjoint_span_commMap_ker, NumberField.FinitePlace.norm_le_one, NumberField.Units.sum_mult_mul_log, Algebra.coe_trace_int, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, FermatLastTheoremForThreeGen.lambda_sq_dvd_c, RingOfIntegers.coe_algebraMap_norm, NumberField.Units.regulator_eq_det', minpoly_coe, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, HeightOneSpectrum.one_lt_absNorm, NumberField.Units.dirichletUnitTheorem.exists_unit, NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, NumberField.Units.complexEmbedding_inj, algebraMap.injective, instIsIntegralClosure, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', NumberField.mixedEmbedding.norm_unit, NumberField.Units.regOfFamily_eq_det', IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime, mapRingEquiv_symm_apply, FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite, NumberField.IsCMField.complexConj_torsion, instCharZero_1, FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd, RingOfIntegers.dvd_norm, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, NumberField.house.basis_repr_norm_le_const_mul_house, NumberField.IsCMField.Units.complexConj_eq_self_iff, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, IsPrimitiveRoot.toInteger_cube_eq_one, IsPrimitiveRoot.zeta_sub_one_prime', NumberField.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, FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd
instMulSemiringAction 📖	CompOp	4 math math: instSMulDistribClass, instIsGaloisGroupIntRingOfIntegersOfRat, 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	39 math math: Rat.RingOfIntegers.isUnit_iff, 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.FinitePlace.norm_lt_one_iff_mem, 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.FinitePlace.mulSupport_finite_int, NumberField.FinitePlace.norm_def_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.FinitePlace.norm_eq_one_iff_notMem, NumberField.isUnit_iff_norm, ext_iff, Rat.ringOfIntegersEquiv_symm_apply_coe, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.norm_le_one, 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 instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring	—	—
coe_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring 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 instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring	—	FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing instIsTorsionFree
coe_mk 📖	—	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 instCommRing CommRing.toRing NumberField.inst_ringOfIntegersAlgebra	—	IsIntegralClosure.isIntegral_algebra instIsIntegralClosure instIsScalarTower_1
extension_isNoetherian 📖	mathematical	—	IsNoetherian NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule NumberField.inst_ringOfIntegersAlgebra	—	IsIntegralClosure.isNoetherian instIsFractionRing instIsScalarTower instIsIntegralClosure instIsScalarTower_1 NumberField.instFiniteDimensional instIsDomain 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 instCommRing	—	SubsemiringClass.instCharZero Subalgebra.instSubsemiringClass NumberField.to_charZero
instCharZero_1 📖	mathematical	—	CharZero NumberField.RingOfIntegers AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing	—	CharZero.of_module
instFreeInt 📖	mathematical	—	Module.Free NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing 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 instCommRing	—	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 instIsDomain IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain
instIsDomain 📖	mathematical	—	IsDomain NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	instIsDomainSubtypeMemSubalgebraIntegralClosure instIsDomain
instIsFractionRing 📖	mathematical	—	IsFractionRing NumberField.RingOfIntegers CommRing.toCommSemiring instCommRing Semifield.toCommSemiring Field.toSemifield instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id	—	integralClosure.isFractionRing_of_finite_extension Rat.isFractionRing Int.instIsDomain NumberField.to_charZero AddCommGroup.intIsScalarTower NumberField.to_finiteDimensional
instIsIntegralClosure 📖	mathematical	—	IsIntegralClosure NumberField.RingOfIntegers instCommRing CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield	—	IsIntegralClosure.tower_top AddCommGroup.intIsScalarTower instIsIntegralClosureInt instIsIntegralInt
instIsIntegralClosureInt 📖	mathematical	—	IsIntegralClosure NumberField.RingOfIntegers Int.instCommRing CommRing.toCommSemiring instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Ring.toIntAlgebra DivisionRing.toRing Field.toDivisionRing instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield	—	integralClosure.isIntegralClosure
instIsIntegralInt 📖	mathematical	—	Algebra.IsIntegral NumberField.RingOfIntegers Int.instCommRing CommRing.toRing instCommRing Ring.toIntAlgebra	—	IsIntegralClosure.isIntegral_algebra instIsIntegralClosureInt AddCommGroup.intIsScalarTower
instIsIntegrallyClosed 📖	mathematical	—	IsIntegrallyClosed NumberField.RingOfIntegers instCommRing	—	integralClosure.isIntegrallyClosedOfFiniteExtension Rat.isFractionRing NumberField.to_charZero AddCommGroup.intIsScalarTower Int.instIsDomain NumberField.to_finiteDimensional
instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors 📖	mathematical	—	IsLocalization NumberField.RingOfIntegers CommRing.toCommSemiring instCommRing Algebra.algebraMapSubmonoid Int.instCommSemiring CommSemiring.toSemiring Ring.toIntAlgebra CommRing.toRing nonZeroDivisors Semiring.toMonoidWithZero Int.instSemiring Semifield.toCommSemiring Field.toSemifield instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id	—	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 instCommRing 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 instCommRing Ring.toSemiring DivisionRing.toRing Field.toDivisionRing instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield	—	IsScalarTower.subalgebra
instIsScalarTower_1 📖	mathematical	—	IsScalarTower NumberField.RingOfIntegers Algebra.toSMul CommRing.toCommSemiring instCommRing CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra Ring.toSemiring DivisionRing.toRing Field.toDivisionRing instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield	—	IsScalarTower.of_algebraMap_eq'
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra	—	Subalgebra.instIsTorsionFree' instIsDomain
instIsTorsionFree_1 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule NumberField.inst_ringOfIntegersAlgebra	—	Module.isTorsionFree_iff_algebraMap_injective instIsDomain algebraMap.injective
instIsTorsionFree_2 📖	mathematical	—	Module.IsTorsionFree NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebra_1 DivisionRing.toRing Field.toDivisionRing	—	Module.IsTorsionFree.trans_faithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instIsDomain instNontrivial instIsTorsionFree_1 instIsTorsionFree instIsScalarTower_1
instNontrivial 📖	mathematical	—	Nontrivial NumberField.RingOfIntegers	—	SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass IsLocalRing.toNontrivial Field.instIsLocalRing
instSMulDistribClass 📖	mathematical	—	SMulDistribClass NumberField.RingOfIntegers SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction CommSemiring.toSemiring CommRing.toCommSemiring instMulSemiringAction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivisionSemiring.toSemiring Algebra.toSMul Ring.toSemiring DivisionRing.toRing Field.toDivisionRing instAlgebra_1 Algebra.id Semifield.toCommSemiring	—	AddGroup.int_smulCommClass' instSMulDistribClassSubtypeMemSubalgebraIntegralClosure
inst_isScalarTower 📖	mathematical	—	IsScalarTower NumberField.RingOfIntegers Algebra.toSMul CommRing.toCommSemiring instCommRing CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra	—	IsScalarTower.of_algHom AlgHom.algHomClass
isIntegral 📖	mathematical	—	IsIntegral NumberField.RingOfIntegers Int.instCommRing CommRing.toRing instCommRing 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 instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 Algebra.id Semifield.toCommSemiring	—	—
ker_algebraMap_eq_bot 📖	mathematical	—	RingHom.ker NumberField.RingOfIntegers RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing 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 instCommRing 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 instCommRing 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 instCommRing 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 instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap instAlgebra_1 Algebra.id Semifield.toCommSemiring	—	—
minpoly_coe 📖	mathematical	—	minpoly Int.instCommRing DivisionRing.toRing Field.toDivisionRing Ring.toIntAlgebra val NumberField.RingOfIntegers CommRing.toRing instCommRing	—	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	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 📖	—	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	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	AddSubgroupClass.sub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubringClass.addSubgroupClass 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 instCommRing NegMemClass.neg_mem SubringClass.toNegMemClass Ring.toSemiring Subalgebra.instSubringClass	—	—
not_isField 📖	mathematical	—	IsField NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	RingHom.injective_int instCharZero_1 NumberField.to_charZero Int.not_isField Algebra.IsIntegral.isField_iff_isField IsIntegralClosure.isIntegral_algebra instIsIntegralClosureInt AddCommGroup.intIsScalarTower instIsDomain
rank 📖	mathematical	—	Module.finrank NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing 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.RingOfIntegers.instCommRing 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.RingOfIntegers.instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringOfIntegersEquiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring semiring RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing instDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield	—	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.RingOfIntegers.instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringOfIntegersEquiv	—	eq_intCast RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass

---

← Back to Index