Documentation Verification Report

TotallyRealComplex

📁 Source: Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

Statistics

Metric	Count
Definitions `IsTotallyComplex`, `IsTotallyReal`, `maximalRealSubfield`	3
Theorems `isTotallyReal_bot`, `complexEmbedding_not_isReal`, `finrank`, `isComplex`, `mult_eq`, `nrRealPlaces_eq_zero`, `complexEmbedding_isReal`, `finrank`, `isReal`, `le_maximalRealSubfield`, `maximalRealSubfield_eq_top`, `mult_eq`, `nrComplexPlaces_eq_zero`, `ofRingEquiv`, `of_algebra`, `instIsAlgebraicSubtypeMemSubfield`, `instIsTotallyRealRat`, `instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic`, `instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic`, `instIsTotallyRealSubtypeMemSubfieldTop`, `isTotallyComplex_iff`, `isTotallyComplex_of_algebra`, `isTotallyReal_iSup`, `isTotallyReal_iff`, `isTotallyReal_iff_le_maximalRealSubfield`, `isTotallyReal_iff_ofRingEquiv`, `isTotallyReal_maximalRealSubfield`, `isTotallyReal_sup`, `isTotallyReal_top_iff`, `maximalRealSubfield_eq_top_iff_isTotallyReal`, `mem_maximalRealSubfield_iff`, `nrComplexPlaces_eq_zero_iff`, `nrRealPlaces_eq_zero_iff`, `isTotallyReal_bot`	34
Total	37

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTotallyReal_bot` 📖	mathematical	—	`NumberField.IsTotallyReal` `IntermediateField` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField`	—	`NumberField.IsTotallyReal.ofRingEquiv` `NumberField.instIsTotallyRealRat` `IsScalarTower.left`

NumberField

Definitions

Name	Category	Theorems
`IsTotallyComplex` 📖	CompData	6 math math: `nrRealPlaces_eq_zero_iff`, `IsCyclotomicExtension.Rat.isTotallyComplex`, `IsCMField.to_isTotallyComplex`, `isTotallyComplex_iff`, `IsCMField.isTotallyComplex`, `isTotallyComplex_of_algebra`
`IsTotallyReal` 📖	CompData	16 math math: `instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic`, `isTotallyReal_sup`, `isTotallyReal_top_iff`, `instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic`, `IsTotallyReal.of_algebra`, `Subfield.isTotallyReal_bot`, `IntermediateField.isTotallyReal_bot`, `isTotallyReal_iff_ofRingEquiv`, `instIsTotallyRealSubtypeMemSubfieldTop`, `isTotallyReal_iff_le_maximalRealSubfield`, `isTotallyReal_iff`, `maximalRealSubfield_eq_top_iff_isTotallyReal`, `isTotallyReal_maximalRealSubfield`, `nrComplexPlaces_eq_zero_iff`, `IsTotallyReal.ofRingEquiv`, `instIsTotallyRealRat`
`maximalRealSubfield` 📖	CompOp	32 math math: `IsCMField.isConj_complexConj`, `IsCMField.zpowers_complexConj_eq_top`, `IsCMField.equivInfinitePlace_symm_apply`, `IsCMField.units_rank_eq_units_rank`, `mem_maximalRealSubfield_iff`, `CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply`, `CMExtension.eq_maximalRealSubfield`, `IsCMField.isQuadraticExtension`, `IsCMField.orderOf_complexConj`, `IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv`, `IsCMField.complexConj_apply_apply`, `IsCMField.coe_ringOfIntegersComplexConj`, `IsCMField.equivInfinitePlace_apply`, `IsCMField.is_quadratic`, `IsCMField.complexConj_apply_eq_self`, `IsCMField.complexEmbedding_complexConj`, `CMExtension.equivMaximalRealSubfield_apply`, `isTotallyReal_iff_le_maximalRealSubfield`, `maximalRealSubfield_eq_top_iff_isTotallyReal`, `IsCMField.card_infinitePlace_eq_card_infinitePlace`, `IsTotallyReal.maximalRealSubfield_eq_top`, `isTotallyReal_maximalRealSubfield`, `IsCMField.ringOfIntegersComplexConj_eq_self_iff`, `IsCMField.mem_realUnits_iff`, `IsCMField.exists_isConj`, `IsCMField.complexConj_eq_self_iff`, `IsTotallyReal.le_maximalRealSubfield`, `IsCMField.RingOfIntegers.complexConj_eq_self_iff`, `IsCMField.infinitePlace_complexConj`, `IsCMField.complexConj_torsion`, `IsCMField.Units.complexConj_eq_self_iff`, `IsCMField.regOfFamily_realFunSystem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsAlgebraicSubtypeMemSubfield` 📖	mathematical	—	`Algebra.IsAlgebraic` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subfield.toField` `DivisionRing.toRing` `Subfield.toAlgebra`	—	`Algebra.IsAlgebraic.tower_top` `SubsemiringClass.instCharZero` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `Subfield.instSubfieldClass` `IsScalarTower.rat`
`instIsTotallyRealRat` 📖	mathematical	—	`IsTotallyReal` `Rat.instField`	—	`Rat.instSubsingletonInfinitePlace` `Rat.isReal_infinitePlace`
`instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic` 📖	mathematical	—	`IsTotallyReal` `IntermediateField` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField`	—	`IsTotallyReal.of_algebra`
`instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `Subfield.toField`	—	`IsTotallyReal.of_algebra`
`instIsTotallyRealSubtypeMemSubfieldTop` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `Top.top` `Subfield.instTop` `Subfield.toField`	—	`isTotallyReal_top_iff`
`isTotallyComplex_iff` 📖	mathematical	—	`IsTotallyComplex` `InfinitePlace.IsComplex`	—	—
`isTotallyComplex_of_algebra` 📖	mathematical	—	`IsTotallyComplex`	—	`InfinitePlace.IsComplex.of_comap` `IsTotallyComplex.isComplex`
`isTotallyReal_iSup` 📖	mathematical	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `Subfield.toField`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Subfield.instCompleteLattice`	—	`isEmpty_or_nonempty` `iSup_of_empty` `Subfield.isTotallyReal_bot` `isTotallyReal_iff_le_maximalRealSubfield` `iSup_le_iff` `IsTotallyReal.le_maximalRealSubfield`
`isTotallyReal_iff` 📖	mathematical	—	`IsTotallyReal` `InfinitePlace.IsReal`	—	—
`isTotallyReal_iff_le_maximalRealSubfield` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `Subfield.toField` `Preorder.toLE` `PartialOrder.toPreorder` `Subfield.instPartialOrder` `maximalRealSubfield`	—	`IsTotallyReal.le_maximalRealSubfield` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `Subfield.instSubfieldClass` `IsScalarTower.of_algebraMap_eq'` `Algebra.IsAlgebraic.tower_bot` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsAlgebraicSubtypeMemSubfield` `IsTotallyReal.of_algebra` `isTotallyReal_maximalRealSubfield`
`isTotallyReal_iff_ofRingEquiv` 📖	mathematical	—	`IsTotallyReal`	—	`IsTotallyReal.ofRingEquiv`
`isTotallyReal_maximalRealSubfield` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `maximalRealSubfield` `Subfield.toField`	—	`InfinitePlace.isReal_iff` `ComplexEmbedding.isReal_iff` `RingHom.ext` `RingHom.star_apply` `instIsAlgebraicSubtypeMemSubfield` `ComplexEmbedding.lift_algebraMap_apply` `Subtype.prop`
`isTotallyReal_sup` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subfield.instCompleteLattice` `Subfield.toField`	—	`isTotallyReal_iff_le_maximalRealSubfield` `sup_le_iff`
`isTotallyReal_top_iff` 📖	mathematical	—	`IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `Top.top` `Subfield.instTop` `Subfield.toField`	—	`isTotallyReal_iff_ofRingEquiv`
`maximalRealSubfield_eq_top_iff_isTotallyReal` 📖	mathematical	—	`maximalRealSubfield` `Top.top` `Subfield` `Field.toDivisionRing` `Subfield.instTop` `IsTotallyReal`	—	`Algebra.IsIntegral.tower_top` `SubsemiringClass.instCharZero` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `Subfield.instSubfieldClass` `IsScalarTower.rat` `Algebra.IsAlgebraic.isIntegral` `isTotallyReal_top_iff` `isTotallyReal_iff_le_maximalRealSubfield` `le_refl` `IsTotallyReal.maximalRealSubfield_eq_top`
`mem_maximalRealSubfield_iff` 📖	mathematical	—	`Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `maximalRealSubfield` `Star.star` `Complex` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `StarRing.toStarAddMonoid` `Complex.instStarRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike`	—	—
`nrComplexPlaces_eq_zero_iff` 📖	mathematical	—	`InfinitePlace.nrComplexPlaces` `IsTotallyReal`	—	—
`nrRealPlaces_eq_zero_iff` 📖	mathematical	—	`InfinitePlace.nrRealPlaces` `IsTotallyComplex`	—	—

NumberField.IsTotallyComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complexEmbedding_not_isReal` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsReal`	—	`Iff.not` `NumberField.InfinitePlace.isReal_mk_iff` `NumberField.InfinitePlace.not_isReal_iff_isComplex` `isComplex`
`finrank` 📖	mathematical	—	`Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero` `NumberField.InfinitePlace.nrComplexPlaces`	—	`NumberField.to_charZero` `NumberField.InfinitePlace.card_add_two_mul_card_eq_rank` `NumberField.nrRealPlaces_eq_zero_iff` `zero_add`
`isComplex` 📖	mathematical	—	`NumberField.InfinitePlace.IsComplex`	—	—
`mult_eq` 📖	mathematical	—	`NumberField.InfinitePlace.mult`	—	`NumberField.InfinitePlace.mult_isComplex` `isComplex`
`nrRealPlaces_eq_zero` 📖	mathematical	—	`NumberField.InfinitePlace.nrRealPlaces`	—	`NumberField.nrRealPlaces_eq_zero_iff`

NumberField.IsTotallyReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complexEmbedding_isReal` 📖	mathematical	—	`NumberField.ComplexEmbedding.IsReal`	—	`NumberField.InfinitePlace.isReal_mk_iff` `isReal`
`finrank` 📖	mathematical	—	`Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero` `NumberField.InfinitePlace.nrRealPlaces`	—	`NumberField.to_charZero` `NumberField.InfinitePlace.card_add_two_mul_card_eq_rank` `NumberField.nrComplexPlaces_eq_zero_iff` `MulZeroClass.mul_zero` `add_zero`
`isReal` 📖	mathematical	—	`NumberField.InfinitePlace.IsReal`	—	—
`le_maximalRealSubfield` 📖	mathematical	—	`Subfield` `Field.toDivisionRing` `Preorder.toLE` `PartialOrder.toPreorder` `Subfield.instPartialOrder` `NumberField.maximalRealSubfield`	—	`RCLike.star_def` `NumberField.ComplexEmbedding.conjugate_coe_eq` `RingHom.congr_fun` `NumberField.ComplexEmbedding.isReal_iff` `NumberField.InfinitePlace.isReal_mk_iff` `isReal`
`maximalRealSubfield_eq_top` 📖	mathematical	—	`NumberField.maximalRealSubfield` `Top.top` `Subfield` `Field.toDivisionRing` `Subfield.instTop`	—	`top_unique` `le_maximalRealSubfield` `NumberField.instIsTotallyRealSubtypeMemSubfieldTop`
`mult_eq` 📖	mathematical	—	`NumberField.InfinitePlace.mult`	—	`NumberField.InfinitePlace.mult_isReal` `isReal`
`nrComplexPlaces_eq_zero` 📖	mathematical	—	`NumberField.InfinitePlace.nrComplexPlaces`	—	`NumberField.nrComplexPlaces_eq_zero_iff`
`ofRingEquiv` 📖	mathematical	—	`NumberField.IsTotallyReal`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `NumberField.InfinitePlace.isReal_comap_iff` `isReal`
`of_algebra` 📖	mathematical	—	`NumberField.IsTotallyReal`	—	`NumberField.InfinitePlace.comap_surjective` `NumberField.InfinitePlace.IsReal.comap` `isReal`

Subfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTotallyReal_bot` 📖	mathematical	—	`NumberField.IsTotallyReal` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField`	—	`bot_eq_of_charZero` `NumberField.IsTotallyReal.ofRingEquiv` `NumberField.instIsTotallyRealRat`

---

← Back to Index