HeightOneSpectrum

📁 Source: Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Statistics

Metric	Count
Definitions HeightOneSpectrum, adicCompletionEquiv, adicCompletionIntegersEquiv, padicEquiv, padicIntEquiv, natGenerator, primesEquiv, withValEquiv, intEquiv, intEquiv	10
Theorems coe_adicCompletionIntegersEquiv_apply, coe_adicCompletionIntegersEquiv_symm_apply, padicEquiv_bijOn, coe_padicIntEquiv_apply, coe_padicIntEquiv_symm_apply, natGenerator_dvd_iff, prime_natGenerator, span_natGenerator, valuation_equiv_padicValuation, intEquiv_apply_eq_ringOfIntegersEquiv, int_algebraMap_injective, int_algebraMap_surjective, instFactPrimeValNat	13
Total	23

IsDedekindDomain

Definitions

Name	Category	Theorems
HeightOneSpectrum 📖	CompData	43 math math: HeightOneSpectrum.equivPrimesOver_apply, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, NumberField.prod_nonarchAbsVal_eq, HeightOneSpectrum.iInf_localization_eq_bot, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Associates.finite_factors, Set.unit_eq, FractionalIdeal.count_finsuppProd, FractionalIdeal.count_finprod_coprime, HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, FractionalIdeal.finprod_heightOneSpectrum_factorization, integer_empty, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, FractionalIdeal.count_finprod, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.maximalIdeal_injective, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.isFinitePlace_iff, NumberField.FinitePlace.coe_apply, Ideal.finite_mulSupport_coe, FiniteAdeleRing.ext_iff, Ideal.finite_mulSupport, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, Ideal.finite_factors, selmerGroup.fromUnit_ker, selmerGroup.fromUnitLift_injective, Ideal.finprod_count, Ideal.finprod_heightOneSpectrum_factorization_coe, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, FractionalIdeal.finite_factors', NumberField.FinitePlace.isFinitePlace, Set.integer_eq, FractionalIdeal.count_maximal, FractionalIdeal.finite_factors, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, integer_univ, Ideal.finprod_not_dvd, Ideal.finite_mulSupport_inv, Ideal.finprod_heightOneSpectrum_factorization, selmerGroup.valuation_ker_eq, FractionalIdeal.finprod_heightOneSpectrum_factorization', HeightOneSpectrum.Support.finite

Padic

Definitions

Name	Category	Theorems
adicCompletionEquiv 📖	CompOp	2 math math: PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply

PadicInt

Definitions

Name	Category	Theorems
adicCompletionIntegersEquiv 📖	CompOp	2 math math: coe_adicCompletionIntegersEquiv_symm_apply, coe_adicCompletionIntegersEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_adicCompletionIntegersEquiv_apply 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.adicCompletion Rat.instField DFunLike.coe Equiv Nat.Primes IsDedekindDomain.HeightOneSpectrum EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Rat.HeightOneSpectrum.primesEquiv ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ContinuousAlgEquiv PadicInt Nat.Prime instFactPrimeValNat Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass instTopologicalSpaceSubtype UniformSpace.Completion.uniformSpace Ring.toIntAlgebra NormedRing.toRing NormedCommRing.toNormedRing CommRing.toRing ValuationSubring.instCommRingSubtypeMem ContinuousAlgEquiv.equivLike adicCompletionIntegersEquiv Padic Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Padic.field NormedField.toNormedCommRing Padic.normedField DivisionRing.toRatAlgebra CauSeq.Completion.Cauchy.divisionRing Rat.linearOrder Rat.instIsStrictOrderedRing padicNorm padicNorm.instIsAbsoluteValueRat Padic.instCharZero IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion Algebra.id Padic.adicCompletionEquiv Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	instFactPrimeValNat Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat Padic.instCharZero EquivLike.toEmbeddingLike Subtype.heq_iff_coe_heq Equiv.apply_symm_apply
coe_adicCompletionIntegersEquiv_symm_apply 📖	mathematical	—	Padic Nat.Prime instFactPrimeValNat Real Real.instLE Norm.norm Padic.instNorm Real.instOne DFunLike.coe ContinuousAlgEquiv IsDedekindDomain.HeightOneSpectrum.adicCompletion Rat.instField Equiv Nat.Primes IsDedekindDomain.HeightOneSpectrum EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Rat.HeightOneSpectrum.primesEquiv ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers PadicInt Int.instCommSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass instTopologicalSpaceSubtype UniformSpace.Completion.uniformSpace CommRing.toCommSemiring instCommRing PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing Ring.toIntAlgebra CommRing.toRing ValuationSubring.instCommRingSubtypeMem NormedRing.toRing NormedCommRing.toNormedRing ContinuousAlgEquiv.equivLike ContinuousAlgEquiv.symm adicCompletionIntegersEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Padic.field NormedField.toNormedCommRing Padic.normedField IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion Algebra.id DivisionRing.toRatAlgebra CauSeq.Completion.Cauchy.divisionRing Rat.linearOrder Rat.instIsStrictOrderedRing padicNorm padicNorm.instIsAbsoluteValueRat Padic.instCharZero Padic.adicCompletionEquiv	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup instFactPrimeValNat SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat Padic.instCharZero Subtype.heq_iff_coe_heq Equiv.apply_symm_apply

Rat

Definitions

Name	Category	Theorems
intEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
int_algebraMap_injective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Int.instCommSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Ring.toIntAlgebra CommRing.toRing	—	Function.Injective.of_comp RingHom.injective_int instCharZero IsScalarTower.algebraMap_eq AddCommGroup.intIsScalarTower
int_algebraMap_surjective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Int.instCommSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Ring.toIntAlgebra CommRing.toRing	—	IsIntegrallyClosed.isIntegral_iff isFractionRing IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain IsIntegral.algebraMap AddCommGroup.intIsScalarTower IsIntegralClosure.isIntegral IsFractionRing.injective

Rat.HeightOneSpectrum

Definitions

Name	Category	Theorems
natGenerator 📖	CompOp	3 math math: prime_natGenerator, natGenerator_dvd_iff, span_natGenerator
primesEquiv 📖	CompOp	6 math math: adicCompletionIntegers.coe_padicIntEquiv_symm_apply, adicCompletion.padicEquiv_bijOn, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, adicCompletionIntegers.coe_padicIntEquiv_apply, valuation_equiv_padicValuation
withValEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natGenerator_dvd_iff 📖	mathematical	—	natGenerator Ideal Int.instSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd CommSemiring.toSemiring CommRing.toCommSemiring EquivLike.toFunLike RingEquiv.instEquivLike Rat.IsIntegralClosure.intEquiv IsDedekindDomain.HeightOneSpectrum.asIdeal	—	span_natGenerator Ideal.mem_span_singleton
prime_natGenerator 📖	mathematical	—	Nat.Prime natGenerator	—	Int.prime_iff_natAbs_prime Submodule.IsPrincipal.prime_generator_of_isPrime Ideal.map_isPrime_of_equiv RingEquiv.instRingEquivClass IsDedekindDomain.HeightOneSpectrum.isPrime Iff.not Ideal.map_eq_bot_iff_of_injective RingEquivClass.toRingHomClass RingEquiv.injective IsDedekindDomain.HeightOneSpectrum.ne_bot
span_natGenerator 📖	mathematical	—	Ideal.span Int.instSemiring Set Set.instSingletonSet natGenerator Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd CommSemiring.toSemiring CommRing.toCommSemiring EquivLike.toFunLike RingEquiv.instEquivLike Rat.IsIntegralClosure.intEquiv IsDedekindDomain.HeightOneSpectrum.asIdeal	—	Nat.cast_natAbs Int.cast_abs Int.instIsStrictOrderedRing Ideal.span_singleton_abs Ideal.span_singleton_generator
valuation_equiv_padicValuation 📖	mathematical	—	Valuation.IsEquiv WithZero Multiplicative DivisionRing.toRing Field.toDivisionRing Rat.instField WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.valuation Rat.padicValuation Nat.Prime DFunLike.coe Equiv IsDedekindDomain.HeightOneSpectrum Nat.Primes EquivLike.toFunLike Equiv.instEquivLike primesEquiv instFactPrimeValNat	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instFactPrimeValNat Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid prime_natGenerator RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Ideal.map_symm IsDedekindDomain.HeightOneSpectrum.ofPrime.congr_simp Rat.padicValuation.congr_simp Ideal.apply_mem_of_equiv_iff map_natCast

Rat.HeightOneSpectrum.adicCompletion

Definitions

Name	Category	Theorems
padicEquiv 📖	CompOp	3 math math: Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, padicEquiv_bijOn, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
padicEquiv_bijOn 📖	mathematical	—	Set.BijOn IsDedekindDomain.HeightOneSpectrum.adicCompletion Rat.instField Padic Nat.Prime DFunLike.coe Equiv IsDedekindDomain.HeightOneSpectrum Nat.Primes EquivLike.toFunLike Equiv.instEquivLike Rat.HeightOneSpectrum.primesEquiv instFactPrimeValNat ContinuousAlgEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace Padic.field PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Padic.normedField IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion Algebra.id DivisionRing.toRatAlgebra CauSeq.Completion.Cauchy.divisionRing Rat.linearOrder Rat.instIsStrictOrderedRing padicNorm padicNorm.instIsAbsoluteValueRat Padic.instCharZero ContinuousAlgEquiv.equivLike padicEquiv SetLike.coe ValuationSubring ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers Subring Padic.instRing Subring.instSetLike PadicInt.subring	—	instFactPrimeValNat Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat Padic.instCharZero SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply PadicInt.norm_le_one Function.Injective.injOn AlgEquiv.injective ContinuousAlgEquiv.surjective

Rat.HeightOneSpectrum.adicCompletionIntegers

Definitions

Name	Category	Theorems
padicIntEquiv 📖	CompOp	2 math math: coe_padicIntEquiv_symm_apply, coe_padicIntEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_padicIntEquiv_apply 📖	mathematical	—	Padic Nat.Prime DFunLike.coe Equiv IsDedekindDomain.HeightOneSpectrum Nat.Primes EquivLike.toFunLike Equiv.instEquivLike Rat.HeightOneSpectrum.primesEquiv instFactPrimeValNat Real Real.instLE Norm.norm Padic.instNorm Real.instOne ContinuousAlgEquiv IsDedekindDomain.HeightOneSpectrum.adicCompletion Rat.instField ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers PadicInt Int.instCommSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass instTopologicalSpaceSubtype UniformSpace.Completion.uniformSpace CommRing.toCommSemiring PadicInt.instCommRing PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing PadicInt.instNormedCommRing Ring.toIntAlgebra CommRing.toRing ValuationSubring.instCommRingSubtypeMem NormedRing.toRing NormedCommRing.toNormedRing ContinuousAlgEquiv.equivLike padicIntEquiv Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Padic.field NormedField.toNormedCommRing Padic.normedField IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion Algebra.id DivisionRing.toRatAlgebra CauSeq.Completion.Cauchy.divisionRing Rat.linearOrder Rat.instIsStrictOrderedRing padicNorm padicNorm.instIsAbsoluteValueRat Padic.instCharZero Rat.HeightOneSpectrum.adicCompletion.padicEquiv	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup instFactPrimeValNat SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass
coe_padicIntEquiv_symm_apply 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.adicCompletion Rat.instField ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers DFunLike.coe ContinuousAlgEquiv PadicInt Nat.Prime Equiv IsDedekindDomain.HeightOneSpectrum Nat.Primes EquivLike.toFunLike Equiv.instEquivLike Rat.HeightOneSpectrum.primesEquiv instFactPrimeValNat Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring PadicInt.instCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing PadicInt.instNormedCommRing SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass instTopologicalSpaceSubtype UniformSpace.Completion.uniformSpace Ring.toIntAlgebra NormedRing.toRing NormedCommRing.toNormedRing CommRing.toRing ValuationSubring.instCommRingSubtypeMem ContinuousAlgEquiv.equivLike ContinuousAlgEquiv.symm padicIntEquiv Padic Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Padic.field NormedField.toNormedCommRing Padic.normedField DivisionRing.toRatAlgebra CauSeq.Completion.Cauchy.divisionRing Rat.linearOrder Rat.instIsStrictOrderedRing padicNorm padicNorm.instIsAbsoluteValueRat Padic.instCharZero IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion Algebra.id Rat.HeightOneSpectrum.adicCompletion.padicEquiv Real Real.instLE Norm.norm Padic.instNorm Real.instOne	—	instFactPrimeValNat Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass

Rat.IsIntegralClosure

Definitions

Name	Category	Theorems
intEquiv 📖	CompOp	3 math math: intEquiv_apply_eq_ringOfIntegersEquiv, Rat.HeightOneSpectrum.natGenerator_dvd_iff, Rat.HeightOneSpectrum.span_natGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intEquiv_apply_eq_ringOfIntegersEquiv 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.RingOfIntegers Rat.instField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike intEquiv NumberField.RingOfIntegers.instAlgebra_1 NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsIntegralClosureInt Rat.ringOfIntegersEquiv	—	NumberField.RingOfIntegers.instIsIntegralClosureInt AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass IsIntegralClosure.isIntegral_algebra Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain Rat.nontrivial NumberField.RingOfIntegers.instIsTorsionFree_2 Classical.choose_eq AlgEquiv.ofAlgHom.congr_simp

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFactPrimeValNat 📖	mathematical	—	Fact Nat.Prime	—	—

---

← Back to Index