MahlerMeasure

📁 Source: Mathlib/NumberTheory/MahlerMeasure.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, card_eq_of_natDegree_le_of_coeff_le, card_mahlerMeasure_le_prod, cyclotomic_dvd_of_mahlerMeasure_eq_one, cyclotomic_mahlerMeasure_eq_one, finite_mahlerMeasure_le, isIntegral_of_mahlerMeasure_eq_one, isPrimitiveRoot_of_mahlerMeasure_eq_one, norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, norm_root_le_one_of_mahlerMeasure_eq_one, one_le_mahlerMeasure_of_ne_zero, pow_eq_one_of_mahlerMeasure_eq_one	12
Total	12

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne	abs instLatticeInt Int.instAddGroup leadingCoeff	—	norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one Nat.cast_one Complex.norm_intCast Real.instIsStrictOrderedRing Int.cast_one RCLike.charZero_rclike eq_intCast RingHom.instRingHomClass leadingCoeff_map_of_injective RingHom.injective_int Complex.instCharZero
card_eq_of_natDegree_le_of_coeff_le 📖	mathematical	—	Set.ncard Polynomial Int.instSemiring setOf natDegree Finset.prod Nat.instCommMonoid Finset.univ Fin.fintype Int.floor Real Real.instRing Real.linearOrder Real.instFloorRing Int.ceil	—	Int.ceil_le Int.le_floor ofFn_natDegree_lt Finset.mem_Icc ofFn_coeff_eq_val_of_lt Set.ncard_congr' Finset.prod_congr Nat.cast_one Set.ncard_coe_finset
card_mahlerMeasure_le_prod 📖	mathematical	—	Set.ncard Polynomial Int.instSemiring setOf natDegree Real Real.instLE mahlerMeasure map Complex Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing NNReal.toReal Finset.prod Nat.instCommMonoid Finset.univ Fin.fintype Nat.floor NNReal instSemiringNNReal instPartialOrderNNReal NNReal.instFloorSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	—
cyclotomic_dvd_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Int.instCommRing X	Ring.toSemiring Int.instRing cyclotomic	—	degree_map_eq_of_injective RingHom.injective_int Complex.instCharZero Splits.exists_eval_eq_zero IsAlgClosed.splits Complex.isAlgClosed Mathlib.Tactic.Contrapose.contrapose₄ coeff_zero_eq_aeval_zero eval_zero_map eq_intCast RingHom.instRingHomClass IsDomain.of_isSimpleRing DivisionRing.isSimpleRing mahlerMeasure_zero NeZero.charZero_one RCLike.charZero_rclike isPrimitiveRoot_of_mahlerMeasure_eq_one cyclotomic_eq_minpoly minpoly.isIntegrallyClosed_dvd Int.instIsDomain IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeIntOfIsAddTorsionFree Complex.instIsAddTorsionFree isIntegral_of_mahlerMeasure_eq_one mem_aroots
cyclotomic_mahlerMeasure_eq_one 📖	mathematical	—	mahlerMeasure map Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.instSemiring algebraMap cyclotomic CommRing.toRing Real Real.instOne	—	eq_or_ne cyclotomic_zero map_one mahlerMeasure_one IsDomain.of_isSimpleRing DivisionRing.isSimpleRing Eq.le IsPrimitiveRoot.norm'_eq_one isPrimitiveRoot_of_mem_primitiveRoots Multiset.prod_eq_one instIsDomain map_cyclotomic mahlerMeasure_eq_leadingCoeff_mul_prod_roots Monic.leadingCoeff cyclotomic.monic CStarRing.norm_of_mem_unitary CStarAlgebra.toCStarRing Complex.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass Multiset.map_congr cyclotomic.roots_eq_primitiveRoots_val NeZero.charZero Complex.instCharZero one_mul
finite_mahlerMeasure_le 📖	mathematical	—	Set.Finite Polynomial Int.instSemiring setOf natDegree Real Real.instLE mahlerMeasure map Complex Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing NNReal.toReal	—	—
isIntegral_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne Multiset Multiset.instMembership aroots Int.instCommRing IsDomain.of_isSimpleRing DivisionRing.isSimpleRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Ring.toIntAlgebra Complex.instRing	IsIntegral	—	IsDomain.of_isSimpleRing DivisionRing.isSimpleRing abs_eq_abs abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one eq_intCast RingHom.instRingHomClass leadingCoeff_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass EuclideanDomain.div_self Int.cast_one Monic.leadingCoeff mul_one Int.cast_neg leadingCoeff_neg mul_neg neg_neg
isPrimitiveRoot_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne Multiset Multiset.instMembership aroots Int.instCommRing IsDomain.of_isSimpleRing DivisionRing.isSimpleRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Ring.toIntAlgebra Complex.instRing	IsPrimitiveRoot CommRing.toCommMonoid	—	IsDomain.of_isSimpleRing DivisionRing.isSimpleRing pow_eq_one_of_mahlerMeasure_eq_one IsPrimitiveRoot.exists_pos
norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne	Norm.norm Complex.instNorm leadingCoeff	—	eq_or_ne map_zero mahlerMeasure_zero NeZero.charZero_one RCLike.charZero_rclike leading_coeff_le_mahlerMeasure leadingCoeff_map_of_injective RingHom.injective_int Complex.instCharZero eq_intCast RingHom.instRingHomClass Nat.cast_one Complex.norm_intCast Real.instIsStrictOrderedRing Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
norm_root_le_one_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne Multiset Multiset.instMembership aroots Int.instCommRing IsDomain.of_isSimpleRing DivisionRing.isSimpleRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Ring.toIntAlgebra Complex.instRing	Real.instLE Norm.norm Complex.instNorm	—	IsDomain.of_isSimpleRing DivisionRing.isSimpleRing le_max_right Multiset.mem_le_prod_of_one_le IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.instZeroLEOneClass le_max_left
one_le_mahlerMeasure_of_ne_zero 📖	mathematical	—	Real Real.instLE Real.instOne mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing	—	le_trans leadingCoeff_map_of_injective RingHom.injective_int Complex.instCharZero eq_intCast RingHom.instRingHomClass Nat.cast_one Complex.norm_intCast Real.instIsStrictOrderedRing Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Int.one_le_abs leadingCoeff_ne_zero leading_coeff_le_mahlerMeasure
pow_eq_one_of_mahlerMeasure_eq_one 📖	mathematical	mahlerMeasure map Complex Int.instSemiring Complex.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Complex.commRing Real Real.instOne Multiset Multiset.instMembership aroots Int.instCommRing IsDomain.of_isSimpleRing DivisionRing.isSimpleRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Ring.toIntAlgebra Complex.instRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instOne	—	IsDomain.of_isSimpleRing DivisionRing.isSimpleRing Complex.instCharZero IntermediateField.charZero Rat.instCharZero IntermediateField.adjoin.finiteDimensional IsIntegral.tower_top AddCommGroup.intIsScalarTower isIntegral_of_mahlerMeasure_eq_one IntermediateField.mem_adjoin_simple_self SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass NumberField.Embeddings.pow_eq_one_of_norm_le_one Complex.isAlgClosed Subtype.coe_ne_coe IntermediateField.coe_isIntegral_iff norm_root_le_one_of_mahlerMeasure_eq_one mem_aroots Int.instIsDomain instIsTorsionFreeIntOfIsAddTorsionFree Complex.instIsAddTorsionFree map_id map_aeval_eq_aeval_map RingHom.ext RingHomCompTriple.comp_eq RingHomCompTriple.ids eq_intCast RingHom.instRingHomClass AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.injective Complex.instNontrivial FaithfulSMul.algebraMap_injective IntermediateField.instFaithfulSMulSubtypeMem Module.Free.instFaithfulSMulOfNontrivial Module.free_of_finite_type_torsion_free' IsPrincipalIdealRing.of_isSimpleRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors

---

← Back to Index