Documentation Verification Report

Extension

📁 Source: FLT/NumberField/InfinitePlace/Extension.lean

Statistics

Metric	Count
Definitions `Extension`, `IsExtension`, `IsMixedExtension`, `IsUnmixedExtension`, `isExtensionEquivSum`, `Extension`, `IsConjugateLift`, `IsLift`, `toRamifiedExtension`, `toUnramifiedExtension`, `RamifiedExtension`, `instCoeExtension`, `UnramifiedExtension`, `instCoeExtension`	14
Theorems `ne`, `not_isExtension_conjugate`, `isExtension`, `isReal`, `not_isReal`, `isReal_of_isReal`, `not_isReal_of_not_isReal`, `isExtension`, `isExtension'`, `isExtension`, `isExtension'`, `isComplex_of_isComplex`, `isExtension_conjugate_of_not_isExtension`, `isExtension_or_isExtension_conjugate`, `isLift_or_isConjugateLift`, `isReal_base`, `mk_embedding`, `comap_eq`, `isComplex`, `isRamified`, `isReal`, `isReal_comap`, `comap_eq`, `isUnramified`	24
Total	38

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
`Extension` 📖	CompOp	19 math math: `Extension.finite`, `finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion`, `adicCompletionComapIntegerLinearEquiv_bijOn`, `tensorAdicCompletionComapAlgHom_bijective`, `tensorAdicCompletionComapLinearMap_isOpenQuotientMap`, `comap_pi_algebra_finite`, `adicCompletionComapAlgEquiv_integral`, `prodAdicCompletionsIntegers_eq_closureIntegers`, `prodAdicCompletionComap_isModuleTopology`, `adicCompletionComapIntegerLinearEquiv_tmul_apply`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_prod_equiv_apply`, `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`, `tensorAdicCompletionComapAlgHom_tmul_apply`

NumberField.ComplexEmbedding

Definitions

Name	Category	Theorems
`IsExtension` 📖	MathDef	13 math math: `NumberField.InfinitePlace.UnramifiedExtension.ofIsUnmixedExtension_embedding_isExtension`, `NumberField.InfinitePlace.Extension.IsConjugateLift.isExtension`, `NumberField.InfinitePlace.Extension.IsLift.isExtension`, `IsMixedExtension.isExtension`, `NumberField.InfinitePlace.UnramifiedExtension.not_isExtension_iff_isExtension_conj`, `NumberField.InfinitePlace.RamifiedExtension.isExtension_conjugate_embedding`, `NumberField.InfinitePlace.Extension.isExtension_or_isExtension_conjugate`, `NumberField.InfinitePlace.Extension.IsLift.isExtension'`, `NumberField.InfinitePlace.Extension.isExtension_algHom`, `NumberField.InfinitePlace.RamifiedExtension.two_mul_card_eq`, `NumberField.InfinitePlace.RamifiedExtension.isExtension_embedding`, `NumberField.InfinitePlace.Extension.IsConjugateLift.isExtension'`, `NumberField.InfinitePlace.UnramifiedExtension.card_eq`
`IsMixedExtension` 📖	MathDef	8 math math: `NumberField.InfinitePlace.RamifiedExtension.isMixedExtension_conjugate`, `NumberField.InfinitePlace.IsUnramified.not_isMixedExtension`, `NumberField.InfinitePlace.IsUnramified.not_isMixedExtension_conjugate`, `NumberField.InfinitePlace.RamifiedExtension.toIsMixedExtension_surjective`, `NumberField.InfinitePlace.RamifiedExtension.toIsMixedExtension_injective`, `NumberField.InfinitePlace.RamifiedExtension.two_mul_card_eq`, `NumberField.InfinitePlace.RamifiedExtension.isMixedExtension`, `NumberField.InfinitePlace.UnramifiedExtension.card_eq`
`IsUnmixedExtension` 📖	MathDef	5 math math: `NumberField.InfinitePlace.UnramifiedExtension.toIsUnmixedExtension_injective`, `NumberField.InfinitePlace.UnramifiedExtension.toIsUnmixedExtension_surjective`, `NumberField.InfinitePlace.UnramifiedExtension.isUnmixedExtension_conjugate`, `NumberField.InfinitePlace.UnramifiedExtension.isUnmixedExtension`, `NumberField.InfinitePlace.UnramifiedExtension.card_eq`
`isExtensionEquivSum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isReal_of_not_isReal` 📖	—	`IsExtension`	—	—	—

NumberField.ComplexEmbedding.IsExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne` 📖	—	`NumberField.ComplexEmbedding.IsExtension`	—	—	—
`not_isExtension_conjugate` 📖	—	`NumberField.ComplexEmbedding.IsExtension`	—	—	—

NumberField.ComplexEmbedding.IsMixedExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExtension` 📖	mathematical	`NumberField.ComplexEmbedding.IsMixedExtension`	`NumberField.ComplexEmbedding.IsExtension`	—	—
`isReal` 📖	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	—	—
`not_isReal` 📖	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	—	—

NumberField.ComplexEmbedding.IsUnmixedExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReal_of_isReal` 📖	—	`NumberField.ComplexEmbedding.IsUnmixedExtension`	—	—	—

NumberField.InfinitePlace

Definitions

Name	Category	Theorems
`Extension` 📖	CompOp	8 math math: `Completion.piEquiv_smul`, `Completion.baseChangeEquiv_tmul`, `Completion.finrank_prod_eq_finrank`, `Completion.piExtension_apply`, `Completion.baseChange_surjective`, `Completion.baseChange_injective`, `Completion.finrank_pi_eq_finrank_tensorProduct`, `Extension.sum_ramificationIdx_eq`
`RamifiedExtension` 📖	CompOp	4 math math: `Extension.card_isUnramified_add_two_mul_card_isRamified`, `RamifiedExtension.toIsMixedExtension_surjective`, `RamifiedExtension.toIsMixedExtension_injective`, `RamifiedExtension.two_mul_card_eq`
`UnramifiedExtension` 📖	CompOp	4 math math: `Extension.card_isUnramified_add_two_mul_card_isRamified`, `UnramifiedExtension.toIsUnmixedExtension_injective`, `UnramifiedExtension.toIsUnmixedExtension_surjective`, `UnramifiedExtension.card_eq`

NumberField.InfinitePlace.Extension

Definitions

Name	Category	Theorems
`IsConjugateLift` 📖	CompData	2 math math: `isLift_or_isConjugateLift`, `NumberField.InfinitePlace.RamifiedExtension.instIsConjugateLiftMkEqComapAlgebraMapValAndIsRamified`
`IsLift` 📖	CompData	3 math math: `NumberField.InfinitePlace.RamifiedExtension.instIsLiftMkEqComapAlgebraMapValAndIsRamified`, `NumberField.InfinitePlace.UnramifiedExtension.instIsLiftMkEqComapAlgebraMapValAndIsUnramifiedOfFactIsReal`, `isLift_or_isConjugateLift`
`toRamifiedExtension` 📖	CompOp	—
`toUnramifiedExtension` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isComplex_of_isComplex` 📖	—	—	—	—	—
`isExtension_conjugate_of_not_isExtension` 📖	—	`NumberField.ComplexEmbedding.IsExtension`	—	—	`isExtension_or_isExtension_conjugate`
`isExtension_or_isExtension_conjugate` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`mk_embedding`
`isLift_or_isConjugateLift` 📖	mathematical	—	`IsLift` `IsConjugateLift`	—	`isExtension_or_isExtension_conjugate`
`isReal_base` 📖	—	—	—	—	`isComplex_of_isComplex`
`mk_embedding` 📖	—	—	—	—	—

NumberField.InfinitePlace.Extension.IsConjugateLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExtension` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`isExtension'`
`isExtension'` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	—

NumberField.InfinitePlace.Extension.IsLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExtension` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`isExtension'`
`isExtension'` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	—

NumberField.InfinitePlace.RamifiedExtension

Definitions

Name	Category	Theorems
`instCoeExtension` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eq` 📖	—	—	—	—	—
`isComplex` 📖	—	—	—	—	`isRamified`
`isRamified` 📖	—	—	—	—	—
`isReal` 📖	—	—	—	—	`isReal_comap` `comap_eq`
`isReal_comap` 📖	—	—	—	—	`isRamified`

NumberField.InfinitePlace.UnramifiedExtension

Definitions

Name	Category	Theorems
`instCoeExtension` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eq` 📖	—	—	—	—	—
`isUnramified` 📖	—	—	—	—	—

---

← Back to Index