Ideal

📁 Source: Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

Statistics

Metric	Count
Definitions	0
Theorems absNorm_span_zeta_sub_one, associated_norm_zeta_sub_one, eq_span_zeta_sub_one_of_liesOver, eq_span_zeta_sub_one_of_liesOver', inertiaDegIn_eq, inertiaDegIn_eq_of_not_dvd, inertiaDegIn_eq_of_prime, inertiaDegIn_eq_of_prime_pow, inertiaDegIn_of_not_dvd, inertiaDeg_eq, inertiaDeg_eq_of_not_dvd, inertiaDeg_eq_of_prime, inertiaDeg_eq_of_prime_pow, inertiaDeg_of_not_dvd, inertiaDeg_span_zeta_sub_one, inertiaDeg_span_zeta_sub_one', isPrime_span_zeta_sub_one, isPrime_span_zeta_sub_one', liesOver_span_zeta_sub_one, map_eq_span_zeta_sub_one_pow, ncard_primesOver_of_prime, ncard_primesOver_of_prime_pow, p_mem_span_zeta_sub_one, ramificationIdxIn_eq, ramificationIdxIn_eq_of_not_dvd, ramificationIdxIn_eq_of_prime, ramificationIdxIn_eq_of_prime_pow, ramificationIdxIn_of_not_dvd, ramificationIdxIn_of_prime, ramificationIdx_eq, ramificationIdx_eq_of_not_dvd, ramificationIdx_eq_of_prime, ramificationIdx_eq_of_prime_pow, ramificationIdx_of_not_dvd, ramificationIdx_span_zeta_sub_one, ramificationIdx_span_zeta_sub_one', span_zeta_sub_one_ne_bot	37
Total	37

IsCyclotomicExtension.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absNorm_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.absNorm_span_singleton Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Int.instNontrivial IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree Algebra.norm_self Ideal.span_singleton_eq_span_singleton associated_norm_zeta_sub_one
associated_norm_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Associated Int.instMonoid DFunLike.coe MonoidHom NumberField.RingOfIntegers MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing NumberField.RingOfIntegers.instCommRing CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' pow_one zero_add IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two Associated.neg_left_iff Associated.refl Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two add_assoc IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two
eq_span_zeta_sub_one_of_liesOver 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.span NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' isPrime_span_zeta_sub_one liesOver_span_zeta_sub_one ncard_primesOver_of_prime_pow
eq_span_zeta_sub_one_of_liesOver' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Ideal.span NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero eq_span_zeta_sub_one_of_liesOver pow_one
inertiaDegIn_eq 📖	mathematical	Monoid.toNatPow Nat.instMonoid	Ideal.inertiaDegIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	NumberField.to_charZero
inertiaDegIn_eq_of_not_dvd 📖	mathematical	—	Ideal.inertiaDegIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Ideal.nonempty_primesOver Int.instIsDomain NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsIntegralInt instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Ideal.IsMaximal.isPrime' Int.ideal_span_isMaximal_of_prime Ideal.inertiaDegIn_eq_inertiaDeg Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois inertiaDeg_eq_of_not_dvd
inertiaDegIn_eq_of_prime 📖	mathematical	—	Ideal.inertiaDegIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero inertiaDegIn_eq_of_prime_pow pow_one
inertiaDegIn_eq_of_prime_pow 📖	mathematical	—	Ideal.inertiaDegIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero IsCyclotomicExtension.isGalois NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec Ideal.inertiaDegIn_eq_inertiaDeg isPrime_span_zeta_sub_one liesOver_span_zeta_sub_one Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois Int.ideal_span_isMaximal_of_prime inertiaDeg_span_zeta_sub_one
inertiaDegIn_of_not_dvd 📖	mathematical	—	Ideal.inertiaDegIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	inertiaDegIn_eq_of_not_dvd
inertiaDeg_eq 📖	mathematical	Monoid.toNatPow Nat.instMonoid	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Ideal.inertiaDegIn_eq_inertiaDeg Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois Int.ideal_span_isMaximal_of_prime inertiaDegIn_eq
inertiaDeg_eq_of_not_dvd 📖	mathematical	—	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	NumberField.to_charZero Nat.Prime.coprime_iff_not_dvd Fact.out IsCyclotomicExtension.zeta_spec RingOfIntegers.exponent_eq_one_iff adjoin_singleton_eq_top Nat.Prime.not_dvd_one NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' Subtype.coe_eta Equiv.symm_apply_apply Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.card pow_one dvd_trans IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain Polynomial.mem_normalizedFactors_iff Polynomial.map_monic_ne_zero minpoly.monic NumberField.RingOfIntegers.isIntegral ZMod.nontrivial Multiset.mem_toFinset Polynomial.map_cyclotomic_int Polynomial.cyclotomic_eq_minpoly NeZero.pos IsPrimitiveRoot.coe_toInteger NumberField.RingOfIntegers.minpoly_coe ZMod.unitOfCoprime.congr_simp orderOf_injective Units.coeHom_injective
inertiaDeg_eq_of_prime 📖	mathematical	—	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec eq_span_zeta_sub_one_of_liesOver' inertiaDeg_span_zeta_sub_one'
inertiaDeg_eq_of_prime_pow 📖	mathematical	—	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec eq_span_zeta_sub_one_of_liesOver inertiaDeg_span_zeta_sub_one
inertiaDeg_of_not_dvd 📖	mathematical	—	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing orderOf ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	inertiaDeg_eq_of_not_dvd
inertiaDeg_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toIntAlgebra	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' liesOver_span_zeta_sub_one Nat.Prime.one_lt Fact.out pow_one IsDomain.toNontrivial IsDedekindDomain.toIsDomain NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Ideal.absNorm_eq_pow_inertiaDeg' Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt NumberField.RingOfIntegers.instNontrivial absNorm_span_zeta_sub_one
inertiaDeg_span_zeta_sub_one' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Ideal.inertiaDeg Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toIntAlgebra	—	NumberField.to_charZero inertiaDeg_span_zeta_sub_one pow_one
isPrime_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.IsPrime NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.span_singleton_prime Prime.ne_zero IsPrimitiveRoot.zeta_sub_one_prime
isPrime_span_zeta_sub_one' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Ideal.IsPrime NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero isPrime_span_zeta_sub_one pow_one
liesOver_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.LiesOver Int.instCommSemiring NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.liesOver_iff Ideal.IsMaximal.eq_of_le Int.ideal_span_isMaximal_of_prime Ideal.IsPrime.ne_top' Ideal.IsPrime.under isPrime_span_zeta_sub_one Ideal.span_singleton_le_iff_mem Ideal.mem_comap algebraMap_int_eq map_natCast RingHom.instRingHomClass p_mem_span_zeta_sub_one
map_eq_span_zeta_sub_one_pow 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.map NumberField.RingOfIntegers RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Int.instCommSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Int.instSemiring RingHom.instFunLike algebraMap Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet Ideal Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Int.instIsDomain NumberField.RingOfIntegers.instIsDomain FractionRing.instFaithfulSMul instFaithfulSMulIntOfCharZero NumberField.RingOfIntegers.instCharZero_1 IsGalois.of_equiv_equiv Algebra.IsSeparable.isAlgebraic Rat.nontrivial IsGalois.to_isSeparable Rat.isFractionRing NumberField.RingOfIntegers.instIsFractionRing RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsFractionRing.algEquiv_commutes AddCommGroup.intIsScalarTower FractionRing.instIsScalarTower IsScalarTower.right OreLocalization.instIsScalarTower NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Ideal.map_span RingHom.instRingHomClass Set.image_singleton Ideal.span_singleton_eq_span_singleton Associated.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Associated.symm associated_norm_zeta_sub_one IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain NumberField.RingOfIntegers.instIsIntegrallyClosed NumberField.RingOfIntegers.instIsIntegralInt instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero Algebra.intNorm_eq_norm NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Algebra.IsIntegral.of_finite Algebra.algebraMap_intNorm_of_isGalois Ideal.prod_span_singleton IsPrimitiveRoot.associated_sub_one_map_sub_one IsPrimitiveRoot.toInteger_isPrimitiveRoot Finset.prod_const Finset.card_univ NumberField.to_finiteDimensional Fintype.card_congr NumberField.RingOfIntegers.instIsIntegralClosureInt Nat.card_eq_fintype_card IsGalois.card_aut_eq_finrank
ncard_primesOver_of_prime 📖	mathematical	—	Set.ncard Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ideal.primesOver Int.instCommSemiring Ideal.span Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero ncard_primesOver_of_prime_pow pow_one
ncard_primesOver_of_prime_pow 📖	mathematical	—	Set.ncard Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ideal.primesOver Int.instCommSemiring Ideal.span Set Set.instSingletonSet Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Nat.Prime.ne_zero Fact.out Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Int.ideal_span_isMaximal_of_prime NumberField.RingOfIntegers.instIsDedekindDomain Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec liesOver_span_zeta_sub_one LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Rat.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsGaloisGroup.card_eq_finrank finrank Nat.totient_prime_pow_succ mul_one ramificationIdx_span_zeta_sub_one inertiaDeg_span_zeta_sub_one Ideal.inertiaDegIn_eq_inertiaDeg isPrime_span_zeta_sub_one Ideal.ramificationIdxIn_eq_ramificationIdx
p_mem_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	NumberField.RingOfIntegers Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt absNorm_span_zeta_sub_one Ideal.absNorm_mem
ramificationIdxIn_eq 📖	mathematical	Monoid.toNatPow Nat.instMonoid	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero
ramificationIdxIn_eq_of_not_dvd 📖	mathematical	—	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Ideal.nonempty_primesOver Int.instIsDomain NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsIntegralInt instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Ideal.IsMaximal.isPrime' Int.ideal_span_isMaximal_of_prime Ideal.ramificationIdxIn_eq_ramificationIdx Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois ramificationIdx_eq_of_not_dvd
ramificationIdxIn_eq_of_prime 📖	mathematical	—	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	NumberField.to_charZero ramificationIdxIn_eq_of_prime_pow pow_one pow_zero one_mul
ramificationIdxIn_eq_of_prime_pow 📖	mathematical	—	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing Monoid.toNatPow Nat.instMonoid	—	NumberField.to_charZero IsCyclotomicExtension.isGalois NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec Ideal.ramificationIdxIn_eq_ramificationIdx isPrime_span_zeta_sub_one liesOver_span_zeta_sub_one Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois ramificationIdx_span_zeta_sub_one
ramificationIdxIn_of_not_dvd 📖	mathematical	—	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	ramificationIdxIn_eq_of_not_dvd
ramificationIdxIn_of_prime 📖	mathematical	—	Ideal.ramificationIdxIn Int.instCommRing Ideal.span Int.instSemiring Set Set.instSingletonSet NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing	—	ramificationIdxIn_eq_of_prime
ramificationIdx_eq 📖	mathematical	Monoid.toNatPow Nat.instMonoid	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet	—	NumberField.to_charZero IsCyclotomicExtension.isGalois Ideal.ramificationIdxIn_eq_ramificationIdx Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain NumberField.to_finiteDimensional instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsDomain instIsGaloisGroupIntRingOfIntegersOfRat IsGaloisGroup.of_isGalois ramificationIdxIn_eq
ramificationIdx_eq_of_not_dvd 📖	mathematical	—	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet	—	NumberField.to_charZero IsCyclotomicExtension.zeta_spec RingOfIntegers.exponent_eq_one_iff adjoin_singleton_eq_top Nat.Prime.not_dvd_one Fact.out NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' Subtype.coe_eta Equiv.symm_apply_apply multiplicity_eq_of_emultiplicity_eq_some le_antisymm Polynomial.emultiplicity_le_one_of_separable Iff.not Polynomial.isUnit_iff_degree_eq_zero LT.lt.ne' Irreducible.degree_pos IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain Polynomial.mem_normalizedFactors_iff Polynomial.map_monic_ne_zero minpoly.monic NumberField.RingOfIntegers.isIntegral ZMod.nontrivial Nat.Prime.one_lt' Multiset.mem_toFinset IsPrimitiveRoot.separable_minpoly_mod IsPrimitiveRoot.toInteger_isPrimitiveRoot NumberField.RingOfIntegers.instIsDomain NumberField.RingOfIntegers.instCharZero_1 ENat.coe_one Order.one_le_iff_pos IsOrderedRing.toZeroLEOneClass NeZero.one emultiplicity_pos_of_dvd
ramificationIdx_eq_of_prime 📖	mathematical	—	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec eq_span_zeta_sub_one_of_liesOver' ramificationIdx_span_zeta_sub_one'
ramificationIdx_eq_of_prime_pow 📖	mathematical	—	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet Monoid.toNatPow Nat.instMonoid	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' IsCyclotomicExtension.zeta_spec eq_span_zeta_sub_one_of_liesOver ramificationIdx_span_zeta_sub_one
ramificationIdx_of_not_dvd 📖	mathematical	—	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet	—	ramificationIdx_eq_of_not_dvd
ramificationIdx_span_zeta_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' isPrime_span_zeta_sub_one Nat.totient_prime_pow_succ Fact.out finrank Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity NumberField.RingOfIntegers.instIsDedekindDomain Ideal.map_ne_bot_of_ne_bot Int.instIsDomain NumberField.RingOfIntegers.instNontrivial instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero NumberField.RingOfIntegers.instCharZero_1 IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Nat.Prime.ne_zero IsScalarTower.right map_eq_span_zeta_sub_one_pow multiplicity_pow_self Ideal.isCancelMulZero span_zeta_sub_one_ne_bot Iff.not Ideal.isUnit_iff Ideal.IsPrime.ne_top
ramificationIdx_span_zeta_sub_one' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Ideal.ramificationIdx Int.instCommRing NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing algebraMap Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsPrimitiveRoot.toInteger NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' pow_one ramificationIdx_span_zeta_sub_one pow_zero one_mul
span_zeta_sub_one_ne_bot 📖	—	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	—	—	NumberField.to_charZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Submodule.ne_bot_iff p_mem_span_zeta_sub_one NeZero.natCast_ne NeZero.charZero NumberField.RingOfIntegers.instCharZero_1

---

← Back to Index