IntegralClosure

📁 Source: FLT/DedekindDomain/IntegralClosure.lean

Statistics

Metric	Count
Definitions fintype, comap, preimageComapFinset, LinearEquivTensorProduct, linearEquivTensorProductModule	5
Theorems sum_ramification_inertia_extensions, finite, intValuation_comap, isTorsionFree, mk_count_factors_map, preimage_comap_finite, ramificationIdx_ne_zero, valuation_comap, LinearEquivTensorProduct_symm_one_tmul, LinearEquivTensorProduct_symm_tmul, linearEquivTensorProductModule_symm_tmul, linearEquivTensorProductModule_tmul, isLocalizedModule	13
Total	18

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_ramification_inertia_extensions 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.Extension IsDedekindDomain.HeightOneSpectrum.Extension.fintype IsDedekindDomain.HeightOneSpectrum.comap	—	IsDedekindDomain.HeightOneSpectrum.isTorsionFree

IsDedekindDomain

Definitions

Name	Category	Theorems
LinearEquivTensorProduct 📖	CompOp	2 math math: LinearEquivTensorProduct_symm_tmul, LinearEquivTensorProduct_symm_one_tmul
linearEquivTensorProductModule 📖	CompOp	2 math math: linearEquivTensorProductModule_tmul, linearEquivTensorProductModule_symm_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LinearEquivTensorProduct_symm_one_tmul 📖	mathematical	—	LinearEquivTensorProduct	—	—
LinearEquivTensorProduct_symm_tmul 📖	mathematical	—	LinearEquivTensorProduct	—	LinearEquivTensorProduct_symm_one_tmul
linearEquivTensorProductModule_symm_tmul 📖	mathematical	—	linearEquivTensorProductModule	—	LinearEquivTensorProduct_symm_one_tmul
linearEquivTensorProductModule_tmul 📖	mathematical	—	linearEquivTensorProductModule	—	linearEquivTensorProductModule_symm_tmul

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
comap 📖	CompOp	26 math math: finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion, adicCompletionComapIntegerLinearEquiv_bijOn, tensorAdicCompletionComapAlgHom_bijective, mk_count_factors_map, IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom, tensorAdicCompletionComapLinearMap_isOpenQuotientMap, comap_pi_algebra_finite, adicCompletionComapAlgEquiv_integral, prodAdicCompletionsIntegers_eq_closureIntegers, prodAdicCompletionComap_isModuleTopology, intValuation_comap, IsDedekindDomain.tendsTo_comap_cofinite, adicCompletionComapIntegerLinearEquiv_tmul_apply, IsDedekindDomain.FiniteAdeleRing.restrictedProduct_prod_equiv_apply, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_apply, valuation_comap, Ideal.sum_ramification_inertia_extensions, instMulActionHomClassAlgHomTensorProductAdicCompletionForallValEqComap, IsDedekindDomain.FiniteAdeleRing.restrictedProduct_pi_isModuleTopology, IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply, instOneHomClassAlgHomTensorProductAdicCompletionForallValEqComap, adicCompletionComapAlgHom_map_closure_is_closed, tensorAdicCompletionComapLinearMap_surjective, preimage_comap_finite, IsDedekindDomain.BaseChange.algebraMap_apply, tensorAdicCompletionComapAlgHom_tmul_apply
preimageComapFinset 📖	CompOp	1 math math: cyclic_base_change

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intValuation_comap 📖	mathematical	—	comap	—	ramificationIdx_ne_zero mk_count_factors_map
isTorsionFree 📖	—	—	—	—	—
mk_count_factors_map 📖	mathematical	—	comap	—	—
preimage_comap_finite 📖	mathematical	—	comap	—	Extension.finite
ramificationIdx_ne_zero 📖	—	—	—	—	—
valuation_comap 📖	mathematical	—	comap	—	intValuation_comap

IsDedekindDomain.HeightOneSpectrum.Extension

Definitions

Name	Category	Theorems
fintype 📖	CompOp	1 math math: Ideal.sum_ramification_inertia_extensions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.Extension	—	IsDedekindDomain.HeightOneSpectrum.isTorsionFree eq_1

IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalizedModule 📖	—	—	—	—	—

---

← Back to Index