Documentation Verification Report

Embeddings

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

Statistics

Metric	Count
Definitions `IsConj`, `IsMixed`, `IsReal`, `embedding`, `IsUnmixed`, `conjugate`, `instFintypeRingHom`, `place`	8
Theorems `comp_eq`, `conjugate_comp_ne`, `not_isReal_of_not_isReal`, `comp`, `eq`, `ext`, `ext_iff`, `isReal_comp`, `coe_embedding_apply`, `comp`, `isConjGal_one`, `isReal_iff_isReal`, `conjugate_coe_eq`, `conjugate_comp`, `exists_comp_symm_eq_of_comp_eq`, `involutive_conjugate`, `isConj_apply_apply`, `isConj_ne_one_iff`, `isConj_one_iff`, `isConj_symm`, `isReal_comp_iff`, `isReal_conjugate_iff`, `isReal_iff`, `lift_algebraMap_apply`, `lift_comp_algebraMap`, `orderOf_isConj_two_of_ne_one`, `place_conjugate`, `card`, `coeff_bdd_of_norm_le`, `finite_of_norm_le`, `instNonemptyRingHom`, `instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed`, `pow_eq_one_of_norm_eq_one`, `pow_eq_one_of_norm_le_one`, `range_eval_eq_rootSet_minpoly`, `place_apply`	36
Total	44

NumberField

Definitions

Name	Category	Theorems
`place` 📖	CompOp	30 math math: `InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal`, `InfinitePlace.isNontrivial`, `InfinitePlace.eq_iff_isEquiv`, `prod_nonarchAbsVal_eq`, `isInfinitePlace_iff`, `InfinitePlace.isometry_embedding`, `InfiniteAdeleRing.algebraMap_apply`, `InfinitePlace.Completion.norm_coe`, `InfinitePlace.coe_apply`, `InfinitePlace.Completion.isometry_extensionEmbedding`, `InfinitePlace.Completion.locallyCompactSpace`, `InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe`, `InfinitePlace.isInfinitePlace`, `InfinitePlace.smul_coe_apply`, `place_apply`, `isFinitePlace_iff`, `FinitePlace.coe_apply`, `count_multisetInfinitePlace_eq_mult`, `InfinitePlace.Completion.extensionEmbedding_coe`, `InfinitePlace.denseRange_algebraMap_pi`, `InfinitePlace.isometry_embedding_of_isReal`, `ComplexEmbedding.place_conjugate`, `InfinitePlace.Completion.extensionEmbedding_of_isReal_coe`, `AdeleRing.algebraMap_fst_apply`, `InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal`, `FinitePlace.isFinitePlace`, `InfinitePlace.Completion.WithAbs.ratCast_equiv`, `prod_archAbsVal_eq`, `InfinitePlace.Completion.Rat.norm_infinitePlace_completion`, `mixedEmbedding.convexBodySum_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`place_apply` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `place` `Norm.norm` `NormedDivisionRing.toNorm` `RingHom` `Semiring.toNonAssocSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `RingHom.instFunLike`	—	—

NumberField.ComplexEmbedding

Definitions

Name	Category	Theorems
`IsConj` 📖	MathDef	7 math math: `NumberField.IsCMField.isConj_complexConj`, `NumberField.InfinitePlace.exists_isConj_of_isRamified`, `isConj_symm`, `NumberField.IsCMField.exists_isConj`, `NumberField.InfinitePlace.mem_stabilizer_mk_iff`, `IsReal.isConjGal_one`, `isConj_one_iff`
`IsMixed` 📖	MathDef	3 math math: `NumberField.InfinitePlace.IsRamified.isMixed_conjugate_embedding`, `NumberField.InfinitePlace.isRamified_mk_iff_isMixed`, `NumberField.InfinitePlace.IsRamified.isMixed_embedding`
`IsReal` 📖	MathDef	19 math math: `isConj_ne_one_iff`, `NumberField.InfinitePlace.isReal_iff`, `NumberField.InfinitePlace.mkReal_coe`, `NumberField.InfinitePlace.not_isReal_of_mk_isComplex`, `NumberField.IsTotallyComplex.complexEmbedding_not_isReal`, `IsConj.isReal_comp`, `NumberField.InfinitePlace.isReal_mk_iff`, `NumberField.InfinitePlace.isReal_of_mk_isReal`, `NumberField.IsTotallyReal.complexEmbedding_isReal`, `NumberField.InfinitePlace.card_real_embeddings`, `NumberField.InfinitePlace.isComplex_iff`, `isReal_iff`, `IsUnmixed.isReal_iff_isReal`, `NumberField.InfinitePlace.mkComplex_coe`, `isReal_comp_iff`, `NumberField.InfinitePlace.isComplex_mk_iff`, `isConj_one_iff`, `NumberField.InfinitePlace.card_complex_embeddings`, `isReal_conjugate_iff`
`IsUnmixed` 📖	MathDef	3 math math: `NumberField.InfinitePlace.IsUnramified.isUnmixed`, `NumberField.InfinitePlace.IsUnramified.isUnmixed_conjugate`, `NumberField.InfinitePlace.isUnramified_mk_iff_isUnmixed`
`conjugate` 📖	CompOp	19 math math: `NumberField.InfinitePlace.IsUnramified.isUnmixed_conjugate`, `conjugate_comp`, `NumberField.InfinitePlace.IsRamified.isMixed_conjugate_embedding`, `NumberField.InfinitePlace.conjugate_embedding_injective`, `involutive_conjugate`, `NumberField.InfinitePlace.mk_eq_iff`, `NumberField.InfinitePlace.IsRamified.comap_embedding_conjugate`, `NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign`, `NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq`, `NumberField.conj_basisMatrix`, `NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal`, `place_conjugate`, `NumberField.InfinitePlace.embedding_mk_eq`, `NumberField.InfinitePlace.mk_conjugate_eq`, `isReal_iff`, `NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd`, `NumberField.canonicalEmbedding.conj_apply`, `conjugate_coe_eq`, `isReal_conjugate_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugate_coe_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `conjugate` `CommSemiring.toSemiring` `Complex.instCommSemiring` `starRingEnd` `Complex.instStarRing`	—	—
`conjugate_comp` 📖	mathematical	—	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `conjugate`	—	—
`exists_comp_symm_eq_of_comp_eq` 📖	mathematical	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Complex.instSemiring` `algebraMap`	`RingHomClass.toRingHom` `AlgEquiv` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm`	—	`IsScalarTower.of_algebraMap_eq'` `RingHom.congr_fun` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsScalarTower.right` `IsGalois.to_normal` `RingHom.ext` `AlgHom.restrictNormal_commutes`
`involutive_conjugate` 📖	mathematical	—	`Function.Involutive` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `conjugate`	—	`star_star`
`isConj_apply_apply` 📖	mathematical	`IsConj`	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	`RingHom.injective` `DivisionRing.isSimpleRing` `Complex.instNontrivial` `IsConj.eq` `RingHomCompTriple.comp_apply` `RingHomInvPair.triples₂` `RingHomInvPair.instStarRingEnd` `RingHomCompTriple.right_ids`
`isConj_ne_one_iff` 📖	mathematical	`IsConj`	`IsReal`	—	`not_iff_not` `isConj_one_iff` `IsConj.ext_iff` `IsReal.isConjGal_one`
`isConj_one_iff` 📖	mathematical	—	`IsConj` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `AlgEquiv.aut` `IsReal`	—	—
`isConj_symm` 📖	mathematical	—	`IsConj` `AlgEquiv.symm` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsConj.symm`
`isReal_comp_iff` 📖	mathematical	—	`IsReal` `RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHom.ext` `RingEquiv.apply_symm_apply` `IsReal.comp`
`isReal_conjugate_iff` 📖	mathematical	—	`IsReal` `conjugate`	—	`IsSelfAdjoint.star_iff`
`isReal_iff` 📖	mathematical	—	`IsReal` `conjugate`	—	`isSelfAdjoint_iff`
`lift_algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `lift` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	—	`RingHom.congr_fun` `lift_comp_algebraMap`
`lift_comp_algebraMap` 📖	mathematical	—	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Complex.instSemiring` `lift` `algebraMap`	—	`Complex.isAlgClosed` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left` `RingHom.algebraMap_toAlgebra'`
`orderOf_isConj_two_of_ne_one` 📖	mathematical	`IsConj`	`orderOf` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut`	—	`orderOf_eq_prime_iff` `Nat.fact_prime_two` `AlgEquiv.ext` `AlgEquiv.coe_pow` `Function.iterate_one` `isConj_apply_apply`
`place_conjugate` 📖	mathematical	—	`NumberField.place` `Complex` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `Complex.instNontrivial` `conjugate`	—	`AbsoluteValue.ext` `Complex.instNontrivial` `Complex.norm_conj`

NumberField.ComplexEmbedding.Extension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	—	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Complex.instSemiring` `RingHom` `algebraMap`	—	—
`conjugate_comp_ne` 📖	—	`NumberField.ComplexEmbedding.IsReal`	—	—	`comp_eq`
`not_isReal_of_not_isReal` 📖	mathematical	`NumberField.ComplexEmbedding.IsReal`	`RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.comp` `algebraMap`	—	`NumberField.ComplexEmbedding.IsReal.comp` `comp_eq`

NumberField.ComplexEmbedding.IsConj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`NumberField.ComplexEmbedding.IsConj`	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHomClass.toRingHom` `AlgEquiv` `Semifield.toCommSemiring` `AlgEquiv.instFunLike` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`RingHom.ext` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `mul_inv_cancel` `one_mul` `RingHom.congr_fun`
`eq` 📖	mathematical	`NumberField.ComplexEmbedding.IsConj`	`DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `RingHom.instFunLike` `AlgEquiv` `Semifield.toCommSemiring` `AlgEquiv.instFunLike` `Star.star` `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`	—	`RingHom.congr_fun`
`ext` 📖	—	`NumberField.ComplexEmbedding.IsConj`	—	—	`AlgEquiv.ext` `RingHom.injective` `DivisionRing.isSimpleRing` `Complex.instNontrivial` `eq`
`ext_iff` 📖	—	`NumberField.ComplexEmbedding.IsConj`	—	—	`ext`
`isReal_comp` 📖	mathematical	`NumberField.ComplexEmbedding.IsConj`	`NumberField.ComplexEmbedding.IsReal` `RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `algebraMap` `Semifield.toCommSemiring`	—	`RingHom.ext` `eq` `AlgEquiv.commutes`

NumberField.ComplexEmbedding.IsReal

Definitions

Name	Category	Theorems
`embedding` 📖	CompOp	1 math math: `coe_embedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_embedding_apply` 📖	mathematical	`NumberField.ComplexEmbedding.IsReal`	`Complex.ofReal` `DFunLike.coe` `RingHom` `Real` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `RingHom.instFunLike` `embedding` `Complex` `Complex.instSemiring`	—	`Complex.ext` `Complex.ofReal_im` `Complex.conj_eq_iff_im` `RingHom.congr_fun`
`comp` 📖	mathematical	`NumberField.ComplexEmbedding.IsReal`	`RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring`	—	`RingHom.ext` `RingHom.congr_fun`
`isConjGal_one` 📖	mathematical	`NumberField.ComplexEmbedding.IsReal`	`NumberField.ComplexEmbedding.IsConj` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `AlgEquiv.aut`	—	`NumberField.ComplexEmbedding.isConj_one_iff`

NumberField.ComplexEmbedding.IsUnmixed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isReal_iff_isReal` 📖	mathematical	`NumberField.ComplexEmbedding.IsUnmixed`	`NumberField.ComplexEmbedding.IsReal` `RingHom.comp` `Complex` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Complex.instSemiring` `algebraMap` `Semifield.toCommSemiring`	—	—

NumberField.Embeddings

Definitions

Name	Category	Theorems
`instFintypeRingHom` 📖	CompOp	12 math math: `NumberField.canonicalEmbedding.integerLattice.inter_ball_finite`, `NumberField.InfinitePlace.card_filter_mk_eq`, `NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign`, `card`, `NumberField.canonicalEmbedding.nnnorm_eq`, `NumberField.discr_eq_basisMatrix_det_sq`, `NumberField.inverse_basisMatrix_mulVec_eq_repr`, `NumberField.InfinitePlace.card_real_embeddings`, `NumberField.canonicalEmbedding.norm_le_iff`, `NumberField.canonicalEmbedding_eq_basisMatrix_mulVec`, `NumberField.InfinitePlace.card_complex_embeddings`, `NumberField.house_eq_sup'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Fintype.card` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instFintypeRingHom` `Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero`	—	`NumberField.to_charZero` `NumberField.to_finiteDimensional` `Fintype.ofEquiv_card` `instIsDomain` `AlgHom.card` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `PerfectField.ofCharZero` `Rat.instCharZero`
`coeff_bdd_of_norm_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike`	`Rat.instNormedField` `Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rat.commRing` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatAlgebra` `NumberField.to_charZero` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instMax` `Real.instOne` `Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `Real.instNatCast` `Nat.choose`	—	`NumberField.to_charZero` `Algebra.IsSeparable.isIntegral` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsSeparable.isAlgebraic` `Rat.nontrivial` `Algebra.IsSeparable.of_integral` `instIsDomain` `Algebra.IsIntegral.of_finite` `NumberField.to_finiteDimensional` `Rat.instCharZero` `PerfectField.ofCharZero` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `Polynomial.coeff_map` `Polynomial.coeff_bdd_of_roots_le` `minpoly.monic` `IsAlgClosed.splits` `minpoly.natDegree_le` `Eq.subset` `Set.instReflSubset` `range_eval_eq_rootSet_minpoly` `Multiset.mem_toFinset`
`finite_of_norm_le` 📖	mathematical	—	`Set.Finite` `setOf` `IsIntegral` `Int.instCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toIntAlgebra`	—	`Real.instIsStrictOrderedRing` `NumberField.to_charZero` `instIsDomain` `Polynomial.bUnion_roots_finite` `Set.finite_Icc` `Set.Finite.subset` `minpoly.isIntegrallyClosed_eq_field_fractions'` `Int.instIsDomain` `Rat.isFractionRing` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `AddCommGroup.intIsScalarTower` `Polynomial.Monic.natDegree_map` `Rat.nontrivial` `minpoly.monic` `minpoly.natDegree_le` `NumberField.to_finiteDimensional` `Set.mem_Icc` `abs_le` `Int.instIsOrderedAddMonoid` `Int.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `LE.le.trans` `Eq.trans_le` `Polynomial.coeff_map` `eq_intCast` `RingHom.instRingHomClass` `Int.norm_cast_rat` `Int.norm_eq_abs` `Int.cast_abs` `coeff_bdd_of_norm_le` `Nat.le_ceil` `Polynomial.mem_rootSet` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `minpoly.ne_zero` `Int.instNontrivial` `minpoly.aeval`
`instNonemptyRingHom` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Fintype.card_pos_iff` `NumberField.to_charZero` `card` `Module.finrank_pos` `commRing_strongRankCondition` `Rat.nontrivial` `NumberField.to_finiteDimensional` `Rat.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`IntermediateField.nonempty_algHom_of_splits` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `IsAlgClosed.splits`
`pow_eq_one_of_norm_eq_one` 📖	mathematical	`IsIntegral` `Int.instCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toIntAlgebra` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `Real` `Real.instOne`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`pow_eq_one_of_norm_le_one` `NeZero.charZero_one` `RCLike.charZero_rclike` `norm_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NumberField.to_charZero` `Rat.isDomain` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsSeparable.isAlgebraic` `Rat.nontrivial` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsSeparable.of_integral` `Algebra.IsIntegral.of_finite` `NumberField.to_finiteDimensional` `Rat.instCharZero` `PerfectField.ofCharZero` `le_of_eq`
`pow_eq_one_of_norm_le_one` 📖	mathematical	`IsIntegral` `Int.instCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toIntAlgebra` `Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `Real.instOne`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Set.Infinite.exists_ne_map_eq_of_mapsTo` `Set.infinite_univ` `instInfiniteNat` `Set.mem_setOf` `IsIntegral.pow` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `pow_le_one₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `finite_of_norm_le` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mul_left_eq_self₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `pow_add` `LT.lt.le` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Ne.lt_or_gt`
`range_eval_eq_rootSet_minpoly` 📖	mathematical	—	`Set.range` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `RingHom.instFunLike` `Polynomial.rootSet` `Rat.commRing` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toRatAlgebra` `NumberField.to_charZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain`	—	`NumberField.to_charZero` `instIsDomain` `Set.ext` `Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly` `NumberField.isAlgebraic`

---

← Back to Index