FiniteAdeleRing

📁 Source: Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Statistics

Metric	Count
Definitions FiniteAdeleRing, algebraMap, instAlgebra, instAlgebra_1, instDFunLikeHeightOneSpectrumAdicCompletion, instCommRingFiniteAdeleRing, instDFunLikeFiniteAdeleRingHeightOneSpectrumAdicCompletion, instTopologicalSpaceFiniteAdeleRing	8
Theorems ext, ext_iff, instIsScalarTower, instIsTopologicalRing, finite	5
Total	13

IsDedekindDomain

Definitions

Name	Category	Theorems
FiniteAdeleRing 📖	CompOp	5 math math: NumberField.AdeleRing.algebraMap_snd_apply, FiniteAdeleRing.instIsScalarTower, FiniteAdeleRing.instIsTopologicalRing, FiniteAdeleRing.ext_iff, NumberField.AdeleRing.algebraMap_fst_apply
instCommRingFiniteAdeleRing 📖	CompOp	2 math math: FiniteAdeleRing.instIsScalarTower, FiniteAdeleRing.instIsTopologicalRing
instDFunLikeFiniteAdeleRingHeightOneSpectrumAdicCompletion 📖	CompOp	1 math math: FiniteAdeleRing.ext_iff
instTopologicalSpaceFiniteAdeleRing 📖	CompOp	1 math math: FiniteAdeleRing.instIsTopologicalRing

IsDedekindDomain.FiniteAdeleRing

Definitions

Name	Category	Theorems
algebraMap 📖	CompOp	—
instAlgebra 📖	CompOp	1 math math: instIsScalarTower
instAlgebra_1 📖	CompOp	1 math math: instIsScalarTower
instDFunLikeHeightOneSpectrumAdicCompletion 📖	CompOp	1 math math: NumberField.AdeleRing.algebraMap_snd_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	DFunLike.coe IsDedekindDomain.FiniteAdeleRing IsDedekindDomain.HeightOneSpectrum IsDedekindDomain.HeightOneSpectrum.adicCompletion IsDedekindDomain.instDFunLikeFiniteAdeleRingHeightOneSpectrumAdicCompletion	—	—	—
ext_iff 📖	mathematical	—	DFunLike.coe IsDedekindDomain.FiniteAdeleRing IsDedekindDomain.HeightOneSpectrum IsDedekindDomain.HeightOneSpectrum.adicCompletion IsDedekindDomain.instDFunLikeFiniteAdeleRingHeightOneSpectrumAdicCompletion	—	ext
instIsScalarTower 📖	mathematical	—	IsScalarTower IsDedekindDomain.FiniteAdeleRing Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semifield.toCommSemiring CommSemiring.toSemiring IsDedekindDomain.instCommRingFiniteAdeleRing instAlgebra instAlgebra_1	—	IsScalarTower.of_algebraMap_eq'
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing IsDedekindDomain.FiniteAdeleRing IsDedekindDomain.instTopologicalSpaceFiniteAdeleRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsDedekindDomain.instCommRingFiniteAdeleRing	—	RestrictedProduct.isTopologicalRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.isOpen_valuationSubring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.Completion.topologicalRing

IsDedekindDomain.HeightOneSpectrum.Support

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite 📖	mathematical	—	Set.Finite IsDedekindDomain.HeightOneSpectrum IsDedekindDomain.HeightOneSpectrum.Support	—	IsLocalization.surj nonZeroDivisors.ne_zero IsDomain.toNontrivial IsDedekindDomain.toIsDomain Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right Ideal.finite_factors Set.Finite.subset Set.mem_setOf_eq IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap IsDedekindDomain.HeightOneSpectrum.intValuation_le_one Mathlib.Tactic.Contrapose.contrapose₁ Valuation.map_mul mul_comm LT.lt.trans_le lt_mul_of_one_lt_right LinearOrderedCommMonoidWithZero.toPosMulStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one WithZero.instNontrivial mul_le_mul_of_nonneg_right MulPosStrictMono.toMulPosMono LinearOrderedCommMonoidWithZero.toMulPosStrictMono

---

← Back to Index