CMField

📁 Source: Mathlib/NumberTheory/NumberField/CMField.lean

Statistics

Metric	Count
Definitions equivMaximalRealSubfield, IsCMField, complexConj, equivInfinitePlace, indexRealUnits, realFundSystem, realUnits, ringOfIntegersComplexConj, starRing, unitsComplexConj, unitsMulComplexConjInv	11
Theorems instIsCMFieldOfTopSetNatRat, isCMField, algebraMap_equivMaximalRealSubfield_symm_apply, eq_maximalRealSubfield, equivMaximalRealSubfield_apply, of_isMulCommutative, complexConj_eq_self_iff, complexConj_eq_self_iff, card_infinitePlace_eq_card_infinitePlace, closure_realFundSystem_sup_torsion, coe_ringOfIntegersComplexConj, complexConj_apply_apply, complexConj_apply_eq_self, complexConj_eq_self_iff, complexConj_ne_one, complexConj_torsion, complexEmbedding_complexConj, equivInfinitePlace_apply, equivInfinitePlace_symm_apply, exists_isConj, indexRealUnits_eq_one_or_two, indexRealUnits_eq_two_iff, indexRealUnits_mul_eq, index_unitsMulComplexConjInv_range_dvd, infinitePlace_complexConj, isConj_complexConj, isConj_eq_isConj, isQuadraticExtension, isTotallyComplex, is_quadratic, map_unitsMulComplexConjInv_torsion, mem_realUnits_iff, ofCMExtension, of_forall_isConj, of_isAbelianGalois, orderOf_complexConj, regOfFamily_realFunSystem, regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv, ringOfIntegersComplexConj_eq_self_iff, to_isTotallyComplex, unitsComplexConj_eq_self_iff, unitsComplexConj_torsion, unitsMulComplexConjInv_apply, unitsMulComplexConjInv_apply_torsion, unitsMulComplexConjInv_ker, units_rank_eq_units_rank, zpowers_complexConj_eq_top	47
Total	58

IsCyclotomicExtension.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCMFieldOfTopSetNatRat 📖	mathematical	—	NumberField.IsCMField	—	isCMField
isCMField 📖	mathematical	Set Set.instMembership	NumberField.IsCMField	—	IsCyclotomicExtension.integral ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat IsCyclotomicExtension.exists_isPrimitiveRoot IntermediateField.charZero Rat.instCharZero IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension isTotallyComplex NumberField.isTotallyComplex_of_algebra IsCyclotomicExtension.isAbelianGalois NumberField.IsCMField.of_isAbelianGalois

NumberField

Definitions

Name	Category	Theorems
IsCMField 📖	CompData	6 math math: IsCyclotomicExtension.Rat.instIsCMFieldOfTopSetNatRat, IsCMField.of_forall_isConj, IsCMField.NumberField.CMExtension.of_isMulCommutative, IsCMField.ofCMExtension, IsCMField.of_isAbelianGalois, IsCyclotomicExtension.Rat.isCMField

NumberField.CMExtension

Definitions

Name	Category	Theorems
equivMaximalRealSubfield 📖	CompOp	2 math math: algebraMap_equivMaximalRealSubfield_symm_apply, equivMaximalRealSubfield_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_equivMaximalRealSubfield_symm_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RingEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equivMaximalRealSubfield SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass Subfield.toAlgebra	—	commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing RingEquiv.apply_symm_apply equivMaximalRealSubfield_apply
eq_maximalRealSubfield 📖	mathematical	—	NumberField.maximalRealSubfield	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing le_antisymm NumberField.IsTotallyReal.le_maximalRealSubfield le_sup_left Subtype.prop IsSimpleOrder.eq_bot_or_eq_top IntermediateField.isSimpleOrder_of_finrank_prime Nat.prime_two Algebra.IsQuadraticExtension.finrank_eq_two Mathlib.Tactic.Contrapose.contrapose₄ sup_eq_left SetLike.coe_set_eq Subfield.coe_toIntermediateField IntermediateField.coe_bot Set.ext Algebra.IsAlgebraic.tower_top SubsemiringClass.instCharZero IsScalarTower.rat Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Rat.instCharZero PerfectField.ofCharZero NumberField.IsTotallyReal.ofRingEquiv NumberField.isTotallyReal_sup NumberField.isTotallyReal_maximalRealSubfield NumberField.instNonemptyInfinitePlaceOfRingHomComplex NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Complex.isAlgClosed NumberField.InfinitePlace.not_isReal_iff_isComplex NumberField.IsTotallyComplex.isComplex NumberField.IsTotallyReal.isReal
equivMaximalRealSubfield_apply 📖	mathematical	—	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equivMaximalRealSubfield RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing

NumberField.IsCMField

Definitions

Name	Category	Theorems
complexConj 📖	CompOp	12 math math: isConj_complexConj, zpowers_complexConj_eq_top, orderOf_complexConj, complexConj_apply_apply, coe_ringOfIntegersComplexConj, complexConj_apply_eq_self, complexEmbedding_complexConj, complexConj_eq_self_iff, RingOfIntegers.complexConj_eq_self_iff, infinitePlace_complexConj, complexConj_torsion, Units.complexConj_eq_self_iff
equivInfinitePlace 📖	CompOp	2 math math: equivInfinitePlace_symm_apply, equivInfinitePlace_apply
indexRealUnits 📖	CompOp	4 math math: regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv, indexRealUnits_mul_eq, indexRealUnits_eq_one_or_two, indexRealUnits_eq_two_iff
realFundSystem 📖	CompOp	2 math math: closure_realFundSystem_sup_torsion, regOfFamily_realFunSystem
realUnits 📖	CompOp	4 math math: closure_realFundSystem_sup_torsion, unitsMulComplexConjInv_ker, mem_realUnits_iff, unitsComplexConj_eq_self_iff
ringOfIntegersComplexConj 📖	CompOp	2 math math: coe_ringOfIntegersComplexConj, ringOfIntegersComplexConj_eq_self_iff
starRing 📖	CompOp	—
unitsComplexConj 📖	CompOp	3 math math: unitsComplexConj_torsion, unitsMulComplexConjInv_apply, unitsComplexConj_eq_self_iff
unitsMulComplexConjInv 📖	CompOp	7 math math: indexRealUnits_mul_eq, unitsMulComplexConjInv_apply_torsion, unitsMulComplexConjInv_ker, unitsMulComplexConjInv_apply, indexRealUnits_eq_two_iff, map_unitsMulComplexConjInv_torsion, index_unitsMulComplexConjInv_range_dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_infinitePlace_eq_card_infinitePlace 📖	mathematical	—	Fintype.card NumberField.InfinitePlace Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField NumberField.InfinitePlace.NumberField.InfinitePlace.fintype NumberField.of_subfield	—	NumberField.of_subfield NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces NumberField.IsTotallyComplex.nrRealPlaces_eq_zero isTotallyComplex NumberField.IsTotallyReal.nrComplexPlaces_eq_zero NumberField.isTotallyReal_maximalRealSubfield Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero PerfectField.ofCharZero zero_add add_zero NumberField.to_charZero NumberField.IsTotallyReal.finrank Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid NumberField.IsTotallyComplex.finrank SubsemiringClass.instCharZero SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass Module.finrank_mul_finrank IsScalarTower.rat commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NumberField.instFiniteDimensional mul_comm Algebra.IsQuadraticExtension.finrank_eq_two isQuadraticExtension
closure_realFundSystem_sup_torsion 📖	mathematical	—	Subgroup Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.closure Set.range NumberField.Units.rank realFundSystem NumberField.Units.torsion realUnits	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MonoidHom.isOfFinOrder realUnits.eq_1 MonoidHom.range_eq_map NumberField.of_subfield NumberField.Units.closure_fundSystem_sup_torsion_eq_top Subgroup.map_sup sup_assoc RingHom.toMonoidHom_eq_coe sup_eq_right MonoidHom.map_closure Set.ext units_rank_eq_units_rank Equiv.exists_congr_left
coe_ringOfIntegersComplexConj 📖	mathematical	—	NumberField.RingOfIntegers.val DFunLike.coe AlgEquiv NumberField.RingOfIntegers Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra Subfield.toAlgebra AlgEquiv.instFunLike ringOfIntegersComplexConj SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring complexConj	—	—
complexConj_apply_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike complexConj	—	NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Rat.instCharZero PerfectField.ofCharZero Complex.isAlgClosed NumberField.ComplexEmbedding.isConj_apply_apply isConj_complexConj
complexConj_apply_eq_self 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike complexConj	—	AlgEquiv.commutes SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass
complexConj_eq_self_iff 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike complexConj	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass zpowers_complexConj_eq_top Subgroup.forall_mem_zpowers MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy IsGalois.fixedField_top Algebra.IsQuadraticExtension.isGalois isQuadraticExtension Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic Algebra.IsQuadraticExtension.normal PerfectField.ofCharZero SubsemiringClass.instCharZero Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Algebra.instFiniteOfIsQuadraticExtension commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IntermediateField.mem_bot IntermediateField.mem_fixedField_iff
complexConj_ne_one 📖	—	—	—	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Rat.instCharZero PerfectField.ofCharZero Complex.isAlgClosed exists_isConj NumberField.ComplexEmbedding.isConj_ne_one_iff NumberField.IsTotallyComplex.complexEmbedding_not_isReal isTotallyComplex
complexConj_torsion 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike complexConj Algebra.IsAlgebraic.isIntegral Rat.instField DivisionRing.toRatAlgebra Algebra.IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Subgroup Units.instGroup Subgroup.instSetLike NumberField.Units.torsion InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	NumberField.Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass Algebra.IsAlgebraic.isIntegral Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero complexEmbedding_complexConj NumberField.Units.complexEmbedding_apply Complex.conj_rootsOfUnity NumberField.Units.instNeZeroNatTorsionOrder Subgroup.apply_coe_mem_map NumberField.Units.map_complexEmbedding_torsion Units.val_inv_eq_inv_val map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
complexEmbedding_complexConj 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Complex.instSemiring RingHom.instFunLike AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass Subfield.toAlgebra AlgEquiv.instFunLike complexConj CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.ComplexEmbedding.IsConj.eq isConj_complexConj RCLike.star_def
equivInfinitePlace_apply 📖	mathematical	—	DFunLike.coe Equiv NumberField.InfinitePlace Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField EquivLike.toFunLike Equiv.instEquivLike equivInfinitePlace NumberField.InfinitePlace.comap algebraMap SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra	—	—
equivInfinitePlace_symm_apply 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real NumberField.InfinitePlace.instFunLikeReal Equiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivInfinitePlace RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Subfield.toAlgebra	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.InfinitePlace.comap_apply equivInfinitePlace_apply Equiv.apply_symm_apply
exists_isConj 📖	mathematical	—	NumberField.ComplexEmbedding.IsConj Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField Subfield.toAlgebra	—	NumberField.InfinitePlace.exists_isConj_of_isRamified Algebra.IsQuadraticExtension.isGalois isQuadraticExtension Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic Algebra.IsQuadraticExtension.normal PerfectField.ofCharZero SubsemiringClass.instCharZero SubringClass.toSubsemiringClass NumberField.InfinitePlace.isRamified_iff NumberField.IsTotallyComplex.isComplex isTotallyComplex NumberField.IsTotallyReal.isReal NumberField.isTotallyReal_maximalRealSubfield
indexRealUnits_eq_one_or_two 📖	mathematical	—	indexRealUnits	—	indexRealUnits_mul_eq Nat.dvd_prime Nat.prime_two index_unitsMulComplexConjInv_range_dvd mul_one two_ne_zero
indexRealUnits_eq_two_iff 📖	mathematical	—	indexRealUnits Subgroup.zpowers Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike unitsMulComplexConjInv Top.top Subgroup.instTop	—	Subgroup.index_eq_one top_le_iff MonoidHom.map_zpowers Subgroup.map_le_range exists_zpow_surjective NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion MonoidHom.range_eq_top Subgroup.eq_top_iff' indexRealUnits_mul_eq two_ne_zero mul_one
indexRealUnits_mul_eq 📖	mathematical	—	indexRealUnits Subgroup.index Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup MonoidHom.range unitsMulComplexConjInv	—	indexRealUnits.eq_1 sup_comm unitsMulComplexConjInv_ker map_unitsMulComplexConjInv_torsion IsCyclic.index_powMonoidHom_range NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion Finite.of_fintype Nat.card_eq_fintype_card Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd NumberField.Units.even_torsionOrder Subgroup.index_map
index_unitsMulComplexConjInv_range_dvd 📖	mathematical	—	Subgroup.index Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup MonoidHom.range unitsMulComplexConjInv	—	IsCyclic.index_powMonoidHom_range NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion Finite.of_fintype Nat.card_eq_fintype_card Even.two_dvd NumberField.Units.even_torsionOrder Subgroup.index_dvd_of_le unitsMulComplexConjInv_apply_torsion pow_two
infinitePlace_complexConj 📖	mathematical	—	DFunLike.coe NumberField.InfinitePlace Real NumberField.InfinitePlace.instFunLikeReal AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike complexConj	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.InfinitePlace.norm_embedding_eq complexEmbedding_complexConj Complex.norm_conj
isConj_complexConj 📖	mathematical	—	NumberField.ComplexEmbedding.IsConj Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField Subfield.toAlgebra complexConj	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass exists_isConj Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Rat.instCharZero PerfectField.ofCharZero NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Complex.isAlgClosed isConj_eq_isConj
isConj_eq_isConj 📖	—	NumberField.ComplexEmbedding.IsConj Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField Subfield.toAlgebra	—	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass IsGalois.card_aut_eq_finrank Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Algebra.instFiniteOfIsQuadraticExtension commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing isQuadraticExtension Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Algebra.IsQuadraticExtension.isGalois Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic Algebra.IsQuadraticExtension.normal PerfectField.ofCharZero SubsemiringClass.instCharZero Algebra.IsQuadraticExtension.finrank_eq_two ExistsUnique.unique Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup Nat.card_eq_two_iff' NumberField.ComplexEmbedding.isConj_ne_one_iff NumberField.IsTotallyComplex.complexEmbedding_not_isReal isTotallyComplex
isQuadraticExtension 📖	mathematical	—	Algebra.IsQuadraticExtension Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass commRing_strongRankCondition EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField SubsemiringClass.nontrivial Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsLocalRing.toNontrivial Field.instIsLocalRing Subfield.toAlgebra	—	is_quadratic
isTotallyComplex 📖	mathematical	—	NumberField.IsTotallyComplex	—	to_isTotallyComplex
is_quadratic 📖	mathematical	—	Algebra.IsQuadraticExtension Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass commRing_strongRankCondition EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField SubsemiringClass.nontrivial Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsLocalRing.toNontrivial Field.instIsLocalRing Subfield.toAlgebra	—	—
map_unitsMulComplexConjInv_torsion 📖	mathematical	—	Subgroup.map Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Subgroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup unitsMulComplexConjInv MonoidHom.range powMonoidHom CommGroup.toCommMonoid Subgroup.toCommGroup Units.instCommGroupUnits CommRing.toCommMonoid	—	SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass MonoidHom.restrict_range MonoidHom.ext unitsMulComplexConjInv_apply_torsion
mem_realUnits_iff 📖	mathematical	—	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike realUnits DFunLike.coe RingHom Subfield Field.toDivisionRing Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap NumberField.inst_ringOfIntegersAlgebra Subfield.toAlgebra Units.val	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ofCMExtension 📖	mathematical	—	NumberField.IsCMField	—	commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass SubsemiringClass.nontrivial Module.Free.of_divisionRing Algebra.finrank_eq_of_equiv_equiv RingHom.ext NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply RingHomCompTriple.comp_eq RingHomCompTriple.right_ids Algebra.IsQuadraticExtension.finrank_eq_two
of_forall_isConj 📖	mathematical	NumberField.ComplexEmbedding.IsConj Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing	NumberField.IsCMField	—	NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField IsGalois.to_isSeparable PerfectField.ofCharZero Rat.instCharZero Complex.isAlgClosed Nat.card_zpowers NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one NumberField.ComplexEmbedding.isConj_ne_one_iff NumberField.IsTotallyComplex.complexEmbedding_not_isReal Nat.finite_of_card_ne_zero ne_of_gt Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Subgroup.smulCommClass_left AlgEquiv.apply_smulCommClass' IsScalarTower.rat NumberField.InfinitePlace.comap_surjective IntermediateField.isAlgebraic_tower_top NumberField.InfinitePlace.mk_embedding NumberField.InfinitePlace.isReal_mk_iff NumberField.ComplexEmbedding.IsConj.isReal_comp IsGaloisGroup.subgroup IsGaloisGroup.of_isGalois Subgroup.mem_zpowers SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing IsGaloisGroup.commutes IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup ofCMExtension
of_isAbelianGalois 📖	mathematical	—	NumberField.IsCMField	—	NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed Complex.instCharZero Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField IsGalois.to_isSeparable IsAbelianGalois.toIsGalois PerfectField.ofCharZero Rat.instCharZero Complex.isAlgClosed NumberField.InfinitePlace.exists_isConj_of_isRamified NumberField.InfinitePlace.isRamified_iff NumberField.IsTotallyComplex.isComplex NumberField.IsTotallyReal.isReal NumberField.instIsTotallyRealRat AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq RingHom.ext eq_ratCast RingHom.instRingHomClass IsAbelianGalois.toIsMulCommutative inv_mul_cancel_comm NumberField.ComplexEmbedding.IsConj.comp of_forall_isConj
orderOf_complexConj 📖	mathematical	—	orderOf AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut complexConj	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass orderOf_eq_prime_iff Nat.fact_prime_two AlgEquiv.ext AlgEquiv.coe_pow Function.iterate_one complexConj_apply_apply complexConj_ne_one
regOfFamily_realFunSystem 📖	mathematical	—	NumberField.Units.regOfFamily realFundSystem Real Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.Units.rank NumberField.Units.regulator Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField NumberField.of_subfield	—	NumberField.of_subfield not_iff_not Equiv.eq_symm_apply units_rank_eq_units_rank Nat.instAtLeastTwoHAddOfNat Finset.prod_const abs_pow Real.instIsOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike NumberField.Units.rank.eq_1 Fintype.card_subtype_compl Fintype.card_unique NumberField.Units.regulator_eq_regOfFamily_fundSystem NumberField.Units.regOfFamily_eq_det NumberField.Units.regOfFamily_eq_det' abs_mul Matrix.det_mul_column Matrix.det_reindex_self Matrix.reindex_apply Matrix.ext Matrix.submatrix_apply Matrix.of_apply SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass equivInfinitePlace_symm_apply NumberField.IsTotallyComplex.mult_eq isTotallyComplex Equiv.apply_symm_apply Subtype.coe_eta NumberField.IsTotallyReal.mult_eq NumberField.isTotallyReal_maximalRealSubfield Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero PerfectField.ofCharZero Nat.cast_one one_mul
regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid NumberField.Units.regulator Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField NumberField.of_subfield Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.Units.rank Real.instInv indexRealUnits	—	NumberField.of_subfield Nat.instAtLeastTwoHAddOfNat indexRealUnits.eq_1 closure_realFundSystem_sup_torsion NumberField.Units.regOfFamily_div_regulator regOfFamily_realFunSystem inv_div mul_div_assoc mul_div_mul_comm div_self ne_of_gt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo one_mul
ringOfIntegersComplexConj_eq_self_iff 📖	mathematical	—	DFunLike.coe AlgEquiv NumberField.RingOfIntegers Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra Subfield.toAlgebra AlgEquiv.instFunLike ringOfIntegersComplexConj Set Set.instMembership Set.range RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass RingOfIntegers.complexConj_eq_self_iff coe_ringOfIntegersComplexConj NumberField.RingOfIntegers.ext_iff AlgEquiv.commutes
to_isTotallyComplex 📖	mathematical	—	NumberField.IsTotallyComplex	—	—
unitsComplexConj_eq_self_iff 📖	mathematical	—	DFunLike.coe MulEquiv Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitsComplexConj Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike realUnits	—	AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass IsScalarTower.algebraMap_apply NumberField.RingOfIntegers.instIsScalarTower_1
unitsComplexConj_torsion 📖	mathematical	—	DFunLike.coe MulEquiv Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitsComplexConj Algebra.IsAlgebraic.isIntegral Rat.instField DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatAlgebra Algebra.IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Field.toSemifield Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.inv	—	NumberField.Units.coe_injective Algebra.IsAlgebraic.isIntegral Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero complexConj_torsion map_units_inv MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
unitsMulComplexConjInv_apply 📖	mathematical	—	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike unitsMulComplexConjInv Units.instMul Units.instInv MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike unitsComplexConj Algebra.IsAlgebraic.isIntegral Rat.instField DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatAlgebra Algebra.IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Field.toSemifield Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero	—	—
unitsMulComplexConjInv_apply_torsion 📖	mathematical	—	DFunLike.coe MonoidHom Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike unitsMulComplexConjInv Monoid.toNatPow	—	Algebra.IsAlgebraic.isIntegral Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero unitsComplexConj_torsion inv_inv pow_two
unitsMulComplexConjInv_ker 📖	mathematical	—	MonoidHom.ker Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Units.instGroup Subgroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup unitsMulComplexConjInv realUnits	—	Subgroup.ext MonoidHom.mem_ker Algebra.IsAlgebraic.isIntegral Algebra.IsSeparable.isAlgebraic Rat.nontrivial Algebra.IsSeparable.of_integral instIsDomain Algebra.IsIntegral.of_finite NumberField.to_finiteDimensional Rat.instCharZero unitsMulComplexConjInv_apply Subgroup.instSubgroupClass OneMemClass.coe_one mul_inv_eq_one unitsComplexConj_eq_self_iff
units_rank_eq_units_rank 📖	mathematical	—	NumberField.Units.rank Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield Subfield.toField NumberField.of_subfield	—	NumberField.of_subfield NumberField.Units.rank.eq_1 card_infinitePlace_eq_card_infinitePlace
zpowers_complexConj_eq_top 📖	mathematical	—	Subgroup.zpowers AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.aut complexConj Top.top Subgroup Subgroup.instTop	—	Subgroup.eq_top_of_card_eq SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass Subgroup.instFiniteSubtypeMem Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Algebra.instFiniteOfIsQuadraticExtension commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing isQuadraticExtension Module.Projective.of_free Algebra.IsQuadraticExtension.toFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Nat.card_zpowers orderOf_complexConj IsGalois.card_aut_eq_finrank Algebra.IsQuadraticExtension.isGalois Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic Algebra.IsQuadraticExtension.normal PerfectField.ofCharZero SubsemiringClass.instCharZero Algebra.IsQuadraticExtension.finrank_eq_two

NumberField.IsCMField.NumberField.CMExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMulCommutative 📖	mathematical	—	NumberField.IsCMField	—	NumberField.IsCMField.of_isAbelianGalois

NumberField.IsCMField.RingOfIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexConj_eq_self_iff 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike NumberField.IsCMField.complexConj NumberField.RingOfIntegers.val RingHom NumberField.RingOfIntegers Subfield.toField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.IsCMField.complexConj_eq_self_iff isIntegral_algebraMap_iff AddCommGroup.intIsScalarTower FaithfulSMul.algebraMap_injective Subfield.instFaithfulSMulSubtypeMem instFaithfulSMul_1 DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing NumberField.RingOfIntegers.isIntegral_coe IsScalarTower.algebraMap_apply NumberField.RingOfIntegers.instIsScalarTower SetLike.coe_mem

NumberField.IsCMField.Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexConj_eq_self_iff 📖	mathematical	—	DFunLike.coe AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike NumberField.maximalRealSubfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subfield.toAlgebra AlgEquiv.instFunLike NumberField.IsCMField.complexConj RingHom NumberField.RingOfIntegers Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing RingHom.instFunLike algebraMap NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Subfield.toField	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff NumberField.Units.coe_coe IsUnit.of_map Algebra.IsIntegral.isLocalHom NumberField.RingOfIntegers.extension_algebra_isIntegral Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsTorsionFree_1 NumberField.RingOfIntegers.ext Units.isUnit

---

← Back to Index