Documentation Verification Report

Dimension

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

Statistics

Metric	Count
Definitions `algEquivComplex`, `instAlgebraValAndEqComapAlgebraMapIsRamified_fLT`, `algEquivComplex`, `algEquivComplexStar`, `algEquivReal`, `instAlgebraValAndEqComapAlgebraMapIsUnramifiedComplexOfIsConjugateLiftMk`, `instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT`, `algEquivComplexOfComplex`, `algEquivComplexOfComplexStar`, `algEquivRealOfReal`, `algebraComplexStar`, `algebraReal`, `instAlgebraComplex_fLT`, `instAlgebraValEqComapAlgebraMap_fLT`, `algHomEquivIsExtension`, `instAlgebraWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace`, `ofIsMixedExtension`, `ofIsMixedExtension_conjugate`, `sumEquivIsMixedExtension`, `toIsMixedExtension`, `equivIsUnmixedExtension`, `instCoeExtension_1`, `ofIsUnmixedExtension`, `toIsUnmixedExtension`, `ramificationIdx`	25
Theorems `extensionEmbedding_algebraMap`, `finrank_eq_two`, `instFactIsComplexValAndEqComapAlgebraMapIsRamified_fLT`, `instIsScalarTowerRealComplex_fLT`, `instIsScalarTowerValAndEqComapAlgebraMapIsRamifiedComplex_fLT`, `extensionEmbeddingOfIsReal_algebraMap`, `extensionEmbedding_algebraMap`, `extensionEmbedding_algebraMap_star`, `finrank_eq_one`, `instFactIsComplexValAndEqComapAlgebraMapIsUnramified_fLT`, `instFactIsRealValAndEqComapAlgebraMapIsUnramified_fLT`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplexOfIsLiftMk`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplex_fLT`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedReal_fLT`, `coe_extensionEmbeddingOfIsReal`, `finrank_eq_ramificationIdx`, `card_isUnramified_add_two_mul_card_isRamified`, `isExtension_algHom`, `sum_ramificationIdx_eq`, `not_isMixedExtension`, `not_isMixedExtension_conjugate`, `instIsConjugateLiftMkEqComapAlgebraMapValAndIsRamified`, `instIsLiftMkEqComapAlgebraMapValAndIsRamified`, `isExtension_conjugate_embedding`, `isExtension_embedding`, `isMixedExtension`, `isMixedExtension_conjugate`, `ofIsMixedExtension_embedding`, `toIsMixedExtension_injective`, `toIsMixedExtension_surjective`, `two_mul_card_eq`, `card_eq`, `instIsLiftMkEqComapAlgebraMapValAndIsUnramifiedOfFactIsReal`, `isComplex_base`, `isReal_of_isReal`, `isUnmixedExtension`, `isUnmixedExtension_conjugate`, `not_isExtension_iff_isExtension_conj`, `ofIsUnmixedExtension_embedding`, `ofIsUnmixedExtension_embedding_isExtension`, `toIsUnmixedExtension_injective`, `toIsUnmixedExtension_ofIsUnmixedExtension`, `toIsUnmixedExtension_surjective`, `comap_embedding_eq_of_isReal`, `comap_mk_of_isExtension`, `ramificationIdx_eq_one`, `ramificationIdx_eq_two`	47
Total	72

NumberField.InfinitePlace

Definitions

Name	Category	Theorems
`ramificationIdx` 📖	CompOp	4 math math: `Completion.finrank_eq_ramificationIdx`, `ramificationIdx_eq_one`, `ramificationIdx_eq_two`, `Extension.sum_ramificationIdx_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_embedding_eq_of_isReal` 📖	—	—	—	—	—
`comap_mk_of_isExtension` 📖	—	`NumberField.ComplexEmbedding.IsExtension`	—	—	—
`ramificationIdx_eq_one` 📖	mathematical	—	`ramificationIdx`	—	`ramificationIdx.eq_1`
`ramificationIdx_eq_two` 📖	mathematical	—	`ramificationIdx`	—	`ramificationIdx.eq_1`

NumberField.InfinitePlace.Completion

Definitions

Name	Category	Theorems
`algEquivComplexOfComplex` 📖	CompOp	—
`algEquivComplexOfComplexStar` 📖	CompOp	—
`algEquivRealOfReal` 📖	CompOp	—
`algebraComplexStar` 📖	CompOp	—
`algebraReal` 📖	CompOp	2 math math: `RamifiedExtension.instIsScalarTowerRealComplex_fLT`, `UnramifiedExtension.instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedReal_fLT`
`instAlgebraComplex_fLT` 📖	CompOp	4 math math: `RamifiedExtension.instIsScalarTowerRealComplex_fLT`, `UnramifiedExtension.instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplex_fLT`, `RamifiedExtension.instIsScalarTowerValAndEqComapAlgebraMapIsRamifiedComplex_fLT`, `UnramifiedExtension.instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplexOfIsLiftMk`
`instAlgebraValEqComapAlgebraMap_fLT` 📖	CompOp	2 math math: `instIsModuleTopologyValEqComapAlgebraMap_fLT`, `finrank_eq_ramificationIdx`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_extensionEmbeddingOfIsReal` 📖	—	—	—	—	—
`finrank_eq_ramificationIdx` 📖	mathematical	—	`instAlgebraValEqComapAlgebraMap_fLT` `NumberField.InfinitePlace.ramificationIdx`	—	`NumberField.InfinitePlace.RamifiedExtension.isReal` `RamifiedExtension.finrank_eq_two` `NumberField.InfinitePlace.RamifiedExtension.isRamified` `UnramifiedExtension.finrank_eq_one` `NumberField.InfinitePlace.UnramifiedExtension.isUnramified`

NumberField.InfinitePlace.Completion.RamifiedExtension

Definitions

Name	Category	Theorems
`algEquivComplex` 📖	CompOp	—
`instAlgebraValAndEqComapAlgebraMapIsRamified_fLT` 📖	CompOp	3 math math: `extensionEmbedding_algebraMap`, `finrank_eq_two`, `instIsScalarTowerValAndEqComapAlgebraMapIsRamifiedComplex_fLT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extensionEmbedding_algebraMap` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsRamified_fLT`	—	`AbsoluteValue.Completion.semialgHomOfComp_coe` `NumberField.InfinitePlace.RamifiedExtension.comap_eq` `NumberField.InfinitePlace.comap_embedding_eq_of_isReal` `NumberField.InfinitePlace.RamifiedExtension.isReal_comap`
`finrank_eq_two` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsRamified_fLT`	—	`instIsScalarTowerRealComplex_fLT`
`instFactIsComplexValAndEqComapAlgebraMapIsRamified_fLT` 📖	—	—	—	—	`NumberField.InfinitePlace.RamifiedExtension.isComplex`
`instIsScalarTowerRealComplex_fLT` 📖	mathematical	—	`NumberField.InfinitePlace.Completion.algebraReal` `NumberField.InfinitePlace.Completion.instAlgebraComplex_fLT`	—	`NumberField.InfinitePlace.Completion.coe_extensionEmbeddingOfIsReal`
`instIsScalarTowerValAndEqComapAlgebraMapIsRamifiedComplex_fLT` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsRamified_fLT` `NumberField.InfinitePlace.Completion.instAlgebraComplex_fLT`	—	`extensionEmbedding_algebraMap`

NumberField.InfinitePlace.Completion.UnramifiedExtension

Definitions

Name	Category	Theorems
`algEquivComplex` 📖	CompOp	—
`algEquivComplexStar` 📖	CompOp	—
`algEquivReal` 📖	CompOp	—
`instAlgebraValAndEqComapAlgebraMapIsUnramifiedComplexOfIsConjugateLiftMk` 📖	CompOp	1 math math: `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplex_fLT`
`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT` 📖	CompOp	7 math math: `extensionEmbedding_algebraMap`, `extensionEmbeddingOfIsReal_algebraMap`, `extensionEmbedding_algebraMap_star`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplex_fLT`, `finrank_eq_one`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedReal_fLT`, `instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplexOfIsLiftMk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extensionEmbeddingOfIsReal_algebraMap` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT`	—	`NumberField.InfinitePlace.Completion.coe_extensionEmbeddingOfIsReal` `extensionEmbedding_algebraMap` `NumberField.InfinitePlace.UnramifiedExtension.instIsLiftMkEqComapAlgebraMapValAndIsUnramifiedOfFactIsReal`
`extensionEmbedding_algebraMap` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT`	—	`NumberField.InfinitePlace.UnramifiedExtension.comap_eq` `AbsoluteValue.Completion.semialgHomOfComp_coe` `NumberField.InfinitePlace.Extension.IsLift.isExtension`
`extensionEmbedding_algebraMap_star` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT`	—	`NumberField.InfinitePlace.UnramifiedExtension.comap_eq` `AbsoluteValue.Completion.semialgHomOfComp_coe` `NumberField.InfinitePlace.Extension.IsConjugateLift.isExtension`
`finrank_eq_one` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT`	—	`instFactIsRealValAndEqComapAlgebraMapIsUnramified_fLT` `NumberField.InfinitePlace.UnramifiedExtension.comap_eq` `NumberField.InfinitePlace.Extension.isLift_or_isConjugateLift` `instFactIsComplexValAndEqComapAlgebraMapIsUnramified_fLT`
`instFactIsComplexValAndEqComapAlgebraMapIsUnramified_fLT` 📖	—	—	—	—	`NumberField.InfinitePlace.Extension.isComplex_of_isComplex` `NumberField.InfinitePlace.UnramifiedExtension.comap_eq`
`instFactIsRealValAndEqComapAlgebraMapIsUnramified_fLT` 📖	—	—	—	—	`NumberField.InfinitePlace.UnramifiedExtension.isReal_of_isReal`
`instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplexOfIsLiftMk` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT` `NumberField.InfinitePlace.Completion.instAlgebraComplex_fLT`	—	`NumberField.InfinitePlace.UnramifiedExtension.comap_eq` `extensionEmbedding_algebraMap`
`instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedComplex_fLT` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT` `instAlgebraValAndEqComapAlgebraMapIsUnramifiedComplexOfIsConjugateLiftMk` `NumberField.InfinitePlace.Completion.instAlgebraComplex_fLT`	—	`NumberField.InfinitePlace.UnramifiedExtension.comap_eq` `extensionEmbedding_algebraMap_star`
`instIsScalarTowerValAndEqComapAlgebraMapIsUnramifiedReal_fLT` 📖	mathematical	—	`instAlgebraValAndEqComapAlgebraMapIsUnramified_fLT` `NumberField.InfinitePlace.Completion.algebraReal`	—	`extensionEmbeddingOfIsReal_algebraMap`

NumberField.InfinitePlace.Extension

Definitions

Name	Category	Theorems
`algHomEquivIsExtension` 📖	CompOp	—
`instAlgebraWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace` 📖	CompOp	1 math math: `isExtension_algHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_isUnramified_add_two_mul_card_isRamified` 📖	mathematical	—	`NumberField.InfinitePlace.UnramifiedExtension` `NumberField.InfinitePlace.RamifiedExtension`	—	`WithAbs.instFiniteDimensional_fLT` `WithAbs.instIsSeparable_fLT` `NumberField.InfinitePlace.RamifiedExtension.two_mul_card_eq` `NumberField.InfinitePlace.UnramifiedExtension.card_eq`
`isExtension_algHom` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension` `instAlgebraWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace`	—	—
`sum_ramificationIdx_eq` 📖	mathematical	—	`NumberField.InfinitePlace.Extension` `NumberField.InfinitePlace.ramificationIdx`	—	`NumberField.InfinitePlace.ramificationIdx_eq_one` `NumberField.InfinitePlace.ramificationIdx_eq_two` `card_isUnramified_add_two_mul_card_isRamified`

NumberField.InfinitePlace.IsUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isMixedExtension` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	—
`not_isMixedExtension_conjugate` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	—

NumberField.InfinitePlace.RamifiedExtension

Definitions

Name	Category	Theorems
`ofIsMixedExtension` 📖	CompOp	1 math math: `ofIsMixedExtension_embedding`
`ofIsMixedExtension_conjugate` 📖	CompOp	—
`sumEquivIsMixedExtension` 📖	CompOp	—
`toIsMixedExtension` 📖	CompOp	2 math math: `toIsMixedExtension_surjective`, `toIsMixedExtension_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsConjugateLiftMkEqComapAlgebraMapValAndIsRamified` 📖	mathematical	—	`NumberField.InfinitePlace.Extension.IsConjugateLift`	—	`isExtension_conjugate_embedding`
`instIsLiftMkEqComapAlgebraMapValAndIsRamified` 📖	mathematical	—	`NumberField.InfinitePlace.Extension.IsLift`	—	`isExtension_embedding`
`isExtension_conjugate_embedding` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`NumberField.ComplexEmbedding.IsExtension.eq_1` `isReal` `comap_eq` `NumberField.InfinitePlace.comap_embedding_eq_of_isReal` `isReal_comap`
`isExtension_embedding` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`NumberField.ComplexEmbedding.IsExtension.eq_1` `comap_eq` `NumberField.InfinitePlace.comap_embedding_eq_of_isReal` `isReal_comap`
`isMixedExtension` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	`isExtension_embedding` `isReal` `isComplex`
`isMixedExtension_conjugate` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsMixedExtension`	—	`isExtension_conjugate_embedding` `isReal` `isComplex`
`ofIsMixedExtension_embedding` 📖	mathematical	`NumberField.ComplexEmbedding.IsMixedExtension`	`ofIsMixedExtension`	—	—
`toIsMixedExtension_injective` 📖	mathematical	—	`NumberField.InfinitePlace.RamifiedExtension` `NumberField.ComplexEmbedding.IsMixedExtension` `toIsMixedExtension`	—	—
`toIsMixedExtension_surjective` 📖	mathematical	—	`NumberField.InfinitePlace.RamifiedExtension` `NumberField.ComplexEmbedding.IsMixedExtension` `toIsMixedExtension`	—	`ofIsMixedExtension_embedding`
`two_mul_card_eq` 📖	mathematical	—	`NumberField.InfinitePlace.RamifiedExtension` `NumberField.ComplexEmbedding.IsMixedExtension` `NumberField.ComplexEmbedding.IsExtension`	—	—

NumberField.InfinitePlace.UnramifiedExtension

Definitions

Name	Category	Theorems
`equivIsUnmixedExtension` 📖	CompOp	—
`instCoeExtension_1` 📖	CompOp	—
`ofIsUnmixedExtension` 📖	CompOp	3 math math: `ofIsUnmixedExtension_embedding_isExtension`, `ofIsUnmixedExtension_embedding`, `toIsUnmixedExtension_ofIsUnmixedExtension`
`toIsUnmixedExtension` 📖	CompOp	3 math math: `toIsUnmixedExtension_injective`, `toIsUnmixedExtension_ofIsUnmixedExtension`, `toIsUnmixedExtension_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq` 📖	mathematical	—	`NumberField.InfinitePlace.UnramifiedExtension` `NumberField.ComplexEmbedding.IsUnmixedExtension` `NumberField.ComplexEmbedding.IsExtension` `NumberField.ComplexEmbedding.IsMixedExtension`	—	—
`instIsLiftMkEqComapAlgebraMapValAndIsUnramifiedOfFactIsReal` 📖	mathematical	—	`NumberField.InfinitePlace.Extension.IsLift` `comap_eq`	—	`comap_eq` `NumberField.InfinitePlace.comap_embedding_eq_of_isReal`
`isComplex_base` 📖	—	—	—	—	`isReal_of_isReal`
`isReal_of_isReal` 📖	—	—	—	—	`isUnramified` `comap_eq`
`isUnmixedExtension` 📖	mathematical	`NumberField.ComplexEmbedding.IsExtension`	`NumberField.ComplexEmbedding.IsUnmixedExtension`	—	`NumberField.InfinitePlace.IsUnramified.not_isMixedExtension` `isUnramified` `comap_eq`
`isUnmixedExtension_conjugate` 📖	mathematical	`NumberField.ComplexEmbedding.IsExtension`	`NumberField.ComplexEmbedding.IsUnmixedExtension`	—	`NumberField.InfinitePlace.Extension.isExtension_conjugate_of_not_isExtension` `comap_eq` `NumberField.InfinitePlace.IsUnramified.not_isMixedExtension_conjugate` `isUnramified`
`not_isExtension_iff_isExtension_conj` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsExtension`	—	`NumberField.InfinitePlace.Extension.isExtension_conjugate_of_not_isExtension` `comap_eq` `isComplex_base`
`ofIsUnmixedExtension_embedding` 📖	mathematical	`NumberField.ComplexEmbedding.IsUnmixedExtension`	`ofIsUnmixedExtension`	—	—
`ofIsUnmixedExtension_embedding_isExtension` 📖	mathematical	`NumberField.ComplexEmbedding.IsUnmixedExtension`	`NumberField.ComplexEmbedding.IsExtension` `ofIsUnmixedExtension`	—	`NumberField.ComplexEmbedding.IsUnmixedExtension.isReal_of_isReal` `not_isExtension_iff_isExtension_conj` `NumberField.ComplexEmbedding.not_isReal_of_not_isReal`
`toIsUnmixedExtension_injective` 📖	mathematical	—	`NumberField.InfinitePlace.UnramifiedExtension` `NumberField.ComplexEmbedding.IsUnmixedExtension` `toIsUnmixedExtension`	—	`isUnmixedExtension` `isUnmixedExtension_conjugate` `NumberField.ComplexEmbedding.IsExtension.ne`
`toIsUnmixedExtension_ofIsUnmixedExtension` 📖	mathematical	`NumberField.ComplexEmbedding.IsUnmixedExtension`	`toIsUnmixedExtension` `ofIsUnmixedExtension`	—	`ofIsUnmixedExtension_embedding_isExtension` `isUnmixedExtension` `isUnmixedExtension_conjugate` `ofIsUnmixedExtension_embedding`
`toIsUnmixedExtension_surjective` 📖	mathematical	—	`NumberField.InfinitePlace.UnramifiedExtension` `NumberField.ComplexEmbedding.IsUnmixedExtension` `toIsUnmixedExtension`	—	`toIsUnmixedExtension_ofIsUnmixedExtension`

---

← Back to Index