Basic

📁 Source: Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean

Statistics

Metric	Count
Definitions boundOfDiscBdd, rankOfDiscrBdd	2
Theorems abs_discr_ge, abs_discr_ge', abs_discr_ge_of_isTotallyComplex, abs_discr_gt_two, abs_discr_rpow_ge_of_isTotallyComplex, discr_eq_basisMatrix_det_sq, exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, finite_of_discr_bdd, finite_of_discr_bdd_of_isComplex, finite_of_discr_bdd_of_isReal, finite_of_finite_generating_set, minkowskiBound_lt_boundOfDiscBdd, natDegree_le_rankOfDiscrBdd, rank_le_rankOfDiscrBdd, covolume_idealLattice, covolume_integerLattice, volume_fundamentalDomain_latticeBasis, sign_discr	19
Total	21

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_discr_ge 📖	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 to_charZero	Real Real.instLE Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow Real.instMonoid Real.pi Real.instIntCast abs instLatticeInt Int.instAddGroup discr	—	to_charZero le_trans Nat.instAtLeastTwoHAddOfNat mul_comm Nat.le_induction le_of_eq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Real.pi_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.isNat_mul Nat.cast_mul one_div Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_add Nat.cast_one one_add_mul_le_pow Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isInt_le_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instNontrivial add_mul Distrib.rightDistribClass pow_succ pow_zero Nat.factorial_pos Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono add_pos' Nat.instIsOrderedAddMonoid pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_add div_pow Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_mul Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono div_le_div₀ lt_trans le_refl mul_le_mul_of_nonneg_right pow_le_pow_right₀ one_le_div Real.pi_le_four InfinitePlace.card_add_two_mul_card_eq_rank abs_discr_ge'
abs_discr_ge' 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast 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 to_charZero Real.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi InfinitePlace.nrComplexPlaces Nat.factorial Real.instIntCast abs instLatticeInt Int.instAddGroup discr	—	to_charZero Nat.instAtLeastTwoHAddOfNat exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr Algebra.coe_norm_int Int.cast_one Int.cast_abs Rat.instIsStrictOrderedRing Rat.cast_intCast Int.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Int.one_le_abs Algebra.norm_ne_zero_iff Int.instIsDomain RingOfIntegers.instIsDomain RingOfIntegers.instFreeInt Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt le_trans mul_comm pow_mul mul_pow div_pow Real.instIsStrictOrderedRing Real.le_sqrt Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono Nat.cast_nonneg' mul_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Nat.cast_pos' Nat.factorial_pos abs_nonneg covariant_swap_add_of_covariant_add mul_one inv_div inv_mul_le_iff₀ Nat.cast_pos Module.finrank_pos commRing_strongRankCondition Rat.nontrivial to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing
abs_discr_ge_of_isTotallyComplex 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast 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 to_charZero Real.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Nat.factorial Real.instIntCast abs instLatticeInt Int.instAddGroup discr	—	to_charZero Nat.instAtLeastTwoHAddOfNat abs_discr_ge' IsTotallyComplex.finrank
abs_discr_gt_two 📖	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 to_charZero	abs instLatticeInt Int.instAddGroup discr	—	to_charZero Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat Int.cast_abs Rat.instIsStrictOrderedRing Rat.cast_abs Real.instIsStrictOrderedRing Rat.cast_intCast lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat CancelDenoms.pow_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.pi_gt_three mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono pow_le_pow_right₀ Real.instZeroLEOneClass le_of_not_gt le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial abs_discr_ge
abs_discr_rpow_ge_of_isTotallyComplex 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast 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 to_charZero Real.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Real.instPow Nat.factorial Real.instInv Real.instIntCast abs instLatticeInt Int.instAddGroup discr	—	to_charZero Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Module.finrank_pos commRing_strongRankCondition Rat.nontrivial to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing Nat.instAtLeastTwoHAddOfNat Real.rpow_le_rpow_iff le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toZeroLEOneClass mul_pos Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Real.rpow_pos_of_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.factorial_pos Real.rpow_nonneg Int.cast_nonneg IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass abs_nonneg Int.instAddLeftMono covariant_swap_add_of_covariant_add Real.div_rpow Real.rpow_mul inv_mul_cancel₀ LT.lt.ne' Real.rpow_one Real.mul_rpow Real.rpow_natCast pow_mul inv_mul_cancel_right₀ Real.rpow_two abs_discr_ge_of_isTotallyComplex
discr_eq_basisMatrix_det_sq 📖	mathematical	—	Complex Complex.instIntCast discr Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Matrix.det RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Embeddings.instFintypeRingHom Complex.instField Complex.instCharZero Complex.commRing basisMatrix	—	Complex.instCharZero Rat.cast_intCast RingOfIntegers.instFreeInt to_charZero Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt coe_discr basisMatrix_eq_embeddingsMatrixReindex Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two to_finiteDimensional Complex.isAlgClosed Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero Equiv.symm_symm Algebra.discr_reindex eq_ratCast RingHom.instRingHomClass
exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr 📖	mathematical	—	FractionalIdeal RingOfIntegers RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield SetLike.instMembership FractionalIdeal.instSetLike Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield RingOfIntegers.instIsFractionRing RingOfIntegers.instIsDedekindDomain Real Real.instLE Real.instRatCast abs Rat.instLattice Rat.addGroup DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra to_charZero Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid MonoidWithZeroHom FractionalIdeal.commSemiring Rat.semiring MonoidWithZeroHom.funLike FractionalIdeal.absNorm RingOfIntegers.instFreeInt Module.IsNoetherian.finite Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing RingOfIntegers.instIsNoetherianInt Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi InfinitePlace.nrComplexPlaces Nat.factorial Module.finrank Algebra.toModule Rat.commSemiring Real.sqrt Real.lattice Real.instAddGroup Real.instIntCast discr	—	RingOfIntegers.instIsFractionRing RingOfIntegers.instIsDedekindDomain to_charZero Complex.instFiniteDimensionalReal Complex.borelSpace le_of_eq mixedEmbedding.convexBodySum_volume ENNReal.ofReal_pow Real.rpow_nonneg ENNReal.toReal_nonneg Real.rpow_natCast Real.rpow_mul div_mul_cancel₀ Nat.cast_ne_zero RCLike.charZero_rclike ne_of_gt Module.finrank_pos commRing_strongRankCondition Rat.nontrivial to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing Real.rpow_one ENNReal.ofReal_toReal ENNReal.mul_ne_top ne_of_lt mixedEmbedding.minkowskiBound_lt_top ENNReal.coe_ne_top mul_comm mul_assoc ENNReal.coe_mul inv_mul_cancel₀ mixedEmbedding.convexBodySumFactor_ne_zero ENNReal.coe_one mul_one RingOfIntegers.instFreeInt Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt Nat.instAtLeastTwoHAddOfNat div_pow mul_comm_div mul_div_assoc' mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis mixedEmbedding.volume_fundamentalDomain_latticeBasis ENNReal.toReal_mul ENNReal.toReal_pow ENNReal.toReal_inv ENNReal.toReal_ofNat mixedEmbedding.finrank ENNReal.toReal_ofReal Rat.cast_nonneg Real.instIsStrictOrderedRing FractionalIdeal.absNorm_nonneg NNReal.coe_natCast inv_div div_eq_mul_inv mul_inv mul_zpow neg_one_mul mul_neg_one neg_neg Real.coe_sqrt sub_eq_add_neg zpow_add₀ two_ne_zero CharZero.NeZero.two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul InfinitePlace.card_add_two_mul_card_eq_rank Nat.cast_add Nat.cast_mul Nat.cast_ofNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isNat_add Int.norm_eq_abs zpow_mul zpow_natCast inv_eq_one_div one_pow Mathlib.Tactic.Ring.pow_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.div_congr Nat.cast_one Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le
exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr 📖	mathematical	—	Real Real.instLE Real.instRatCast abs Rat.instLattice Rat.addGroup DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing MonoidHom.instFunLike Algebra.norm DivisionRing.toRatAlgebra to_charZero RingOfIntegers.val Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi InfinitePlace.nrComplexPlaces Nat.factorial 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 Real.sqrt Real.lattice Real.instAddGroup Real.instIntCast discr	—	RingOfIntegers.instIsFractionRing RingOfIntegers.instIsDedekindDomain to_charZero RingOfIntegers.instFreeInt Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt Nat.instAtLeastTwoHAddOfNat exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr FractionalIdeal.mem_one_iff ne_zero_of_map MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul Rat.cast_one FractionalIdeal.absNorm_one
finite_of_discr_bdd 📖	mathematical	—	Set.Finite IntermediateField Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing FiniteDimensional SetLike.instMembership IntermediateField.instSetLike Rat.instDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.toField IntermediateField.module' DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Algebra.toSMul Rat.commSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule Semifield.toDivisionSemiring Field.toSemifield IsScalarTower.rat SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Rat.instNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace setOf abs instLatticeInt Int.instAddGroup discr CharZero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IntermediateField.charZero Rat.instCharZero Subtype.prop	—	Set.Finite.subset IsScalarTower.rat IntermediateField.charZero Rat.instCharZero Subtype.prop Set.Finite.union hermiteTheorem.finite_of_discr_bdd_of_isReal hermiteTheorem.finite_of_discr_bdd_of_isComplex SubsemiringClass.instCharZero SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass instNonemptyInfinitePlaceOfRingHomComplex Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed Set.mem_union_left Set.mem_union_right InfinitePlace.not_isReal_iff_isComplex
sign_discr 📖	mathematical	—	discr Monoid.toNatPow Int.instMonoid InfinitePlace.nrComplexPlaces	—	Complex.instCharZero discr_eq_basisMatrix_det_sq Complex.sq_nonneg_iff Complex.conj_eq_iff_im RingHom.map_det RingHom.mapMatrix_apply ComplexEmbedding.involutive_conjugate conj_basisMatrix Matrix.reindex_apply Equiv.refl_symm Equiv.coe_refl Function.Involutive.toPerm_symm Matrix.det_permute' mul_eq_right₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain det_of_basisMatrix_non_zero InfinitePlace.ComplexEmbedding.conjugate_sign Int.cast_pow Int.cast_neg Int.cast_one neg_one_pow_eq_one_iff_even Mathlib.Meta.NormNum.isInt_eq_false Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.neg_one_pow Int.cast_nonneg IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid RCLike.toZeroLEOneClass LT.lt.le Odd.neg_one_pow Nat.not_even_iff_odd Int.cast_nonneg_iff NeZero.charZero_one not_le

NumberField.hermiteTheorem

Definitions

Name	Category	Theorems
boundOfDiscBdd 📖	CompOp	1 math math: minkowskiBound_lt_boundOfDiscBdd
rankOfDiscrBdd 📖	CompOp	2 math math: natDegree_le_rankOfDiscrBdd, rank_le_rankOfDiscrBdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_discr_bdd_of_isComplex 📖	mathematical	—	Set.Finite IntermediateField Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing FiniteDimensional SetLike.instMembership IntermediateField.instSetLike Rat.instDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.toField IntermediateField.module' DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Algebra.toSMul Rat.commSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule Semifield.toDivisionSemiring Field.toSemifield IsScalarTower.rat SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Rat.instNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace setOf Set.Nonempty NumberField.InfinitePlace NumberField.InfinitePlace.IsComplex abs instLatticeInt Int.instAddGroup NumberField.discr CharZero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IntermediateField.charZero Rat.instCharZero Subtype.prop	—	finite_of_finite_generating_set IsScalarTower.rat IntermediateField.charZero Rat.instCharZero Subtype.prop instIsDomain Polynomial.bUnion_roots_finite Set.finite_Icc SubsemiringClass.instCharZero SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain minkowskiBound_lt_boundOfDiscBdd one_mul mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Nat.cast_one NumberField.mixedEmbedding.one_le_convexBodyLT'Factor NumberField.to_charZero NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex NumberField.RingOfIntegers.isIntegral_coe AddCommGroup.intIsScalarTower natDegree_le_rankOfDiscrBdd 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 minpoly.isIntegrallyClosed_eq_field_fractions' Int.instIsDomain Rat.isFractionRing IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain Polynomial.coeff_map eq_intCast RingHom.instRingHomClass Int.norm_cast_rat Int.norm_eq_abs Int.cast_abs Real.instIsStrictOrderedRing NumberField.Embeddings.coeff_bdd_of_norm_le Complex.isAlgClosed Complex.instCharZero NumberField.InfinitePlace.le_iff_le le_of_lt le_trans NNReal.val_eq_coe NNReal.coe_mul NNReal.coe_pow NNReal.coe_max NNReal.coe_one Real.coe_sqrt NNReal.coe_add mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono pow_le_pow_right₀ le_max_right rank_le_rankOfDiscrBdd NNReal.coe_natCast Nat.cast_le Nat.choose_le_choose Nat.choose_le_middle Nat.cast_nonneg' pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_max_of_lt_left Real.sqrt_pos_of_pos add_pos' Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.Positivity.nnreal_coe_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add NNReal.addLeftMono mul_nonneg NNReal.instIsOrderedRing zero_le NNReal.instCanonicallyOrderedAdd NNReal.instIsStrictOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Nat.le_ceil Polynomial.mem_rootSet instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero minpoly.ne_zero Int.instNontrivial Polynomial.aeval_algebraMap_eq_zero_iff instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.aeval IntermediateField.lift_top IsScalarTower.left IntermediateField.lift_adjoin Set.image_singleton IntermediateField.lift_injective
finite_of_discr_bdd_of_isReal 📖	mathematical	—	Set.Finite IntermediateField Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing FiniteDimensional SetLike.instMembership IntermediateField.instSetLike Rat.instDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.toField IntermediateField.module' DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Algebra.toSMul Rat.commSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule Semifield.toDivisionSemiring Field.toSemifield IsScalarTower.rat SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Rat.instNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace setOf Set.Nonempty NumberField.InfinitePlace NumberField.InfinitePlace.IsReal abs instLatticeInt Int.instAddGroup NumberField.discr CharZero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IntermediateField.charZero Rat.instCharZero Subtype.prop	—	finite_of_finite_generating_set IsScalarTower.rat IntermediateField.charZero Rat.instCharZero Subtype.prop instIsDomain Polynomial.bUnion_roots_finite Set.finite_Icc SubsemiringClass.instCharZero SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain minkowskiBound_lt_boundOfDiscBdd one_mul mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Nat.cast_one NumberField.mixedEmbedding.one_le_convexBodyLTFactor NumberField.to_charZero NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal NumberField.RingOfIntegers.isIntegral_coe AddCommGroup.intIsScalarTower natDegree_le_rankOfDiscrBdd 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 minpoly.isIntegrallyClosed_eq_field_fractions' Int.instIsDomain Rat.isFractionRing IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain Polynomial.coeff_map eq_intCast RingHom.instRingHomClass Int.norm_cast_rat Int.norm_eq_abs Int.cast_abs Real.instIsStrictOrderedRing NumberField.Embeddings.coeff_bdd_of_norm_le Complex.isAlgClosed Complex.instCharZero NumberField.InfinitePlace.le_iff_le le_of_lt le_trans NNReal.coe_max sup_of_le_left NNReal.val_eq_coe NNReal.coe_mul NNReal.coe_pow NNReal.coe_one NNReal.coe_natCast mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono pow_le_pow_right₀ le_max_right rank_le_rankOfDiscrBdd Nat.mono_cast Nat.choose_le_choose Nat.choose_le_middle Nat.cast_nonneg' pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_max_of_lt_left Mathlib.Meta.Positivity.nnreal_coe_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add NNReal.addLeftMono mul_nonneg NNReal.instIsOrderedRing zero_le NNReal.instCanonicallyOrderedAdd NNReal.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.le_ceil Polynomial.mem_rootSet instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero minpoly.ne_zero Int.instNontrivial Polynomial.aeval_algebraMap_eq_zero_iff instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.aeval IntermediateField.lift_top IsScalarTower.left IntermediateField.lift_adjoin Set.image_singleton IntermediateField.lift_injective
finite_of_finite_generating_set 📖	mathematical	Set Set.instMembership IntermediateField Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing IntermediateField.adjoin Set.instSingletonSet	Set.Finite	—	Set.finite_coe_iff Finite.of_injective Subtype.mem
minkowskiBound_lt_boundOfDiscBdd 📖	mathematical	abs instLatticeInt Int.instAddGroup NumberField.discr	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder NumberField.mixedEmbedding.minkowskiBound Units FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Units.instOne ENNReal.ofNNReal boundOfDiscBdd	—	add_tsub_cancel_right NNReal.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftReflectLT IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono NNReal.addLeftMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing lt_of_le_of_lt NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.mixedEmbedding.minkowskiBound.eq_1 NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis boundOfDiscBdd.eq_1 Units.val_one FractionalIdeal.absNorm_one Rat.cast_one ENNReal.ofReal_one one_mul NumberField.to_charZero NumberField.mixedEmbedding.finrank Nat.instAtLeastTwoHAddOfNat NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis ENNReal.coe_mul ENNReal.coe_pow ENNReal.coe_ofNat mul_le_mul' IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid covariant_swap_mul_of_covariant_mul pow_le_one₀ IsOrderedRing.toPosMulMono ENNReal.instIsOrderedRing zero_le ENNReal.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instCharZero ENNReal.coe_le_coe_of_le NNReal.coe_le_coe coe_nnnorm Int.norm_eq_abs Int.cast_abs Real.instIsStrictOrderedRing NNReal.coe_natCast Int.cast_natCast Int.cast_le Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike pow_le_pow_right' one_le_two rank_le_rankOfDiscrBdd ENNReal.coe_lt_coe
natDegree_le_rankOfDiscrBdd 📖	mathematical	abs instLatticeInt Int.instAddGroup NumberField.discr IntermediateField.adjoin Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero Set Set.instSingletonSet NumberField.RingOfIntegers.val Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing minpoly DivisionRing.toRing Ring.toIntAlgebra rankOfDiscrBdd	—	NumberField.to_charZero rank_le_rankOfDiscrBdd Polynomial.Monic.natDegree_map Rat.nontrivial minpoly.monic NumberField.RingOfIntegers.isIntegral_coe minpoly.isIntegrallyClosed_eq_field_fractions' Int.instIsDomain Rat.isFractionRing IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsDomain AddCommGroup.intIsScalarTower Field.primitive_element_iff_minpoly_natDegree_eq NumberField.to_finiteDimensional
rank_le_rankOfDiscrBdd 📖	mathematical	abs instLatticeInt Int.instAddGroup NumberField.discr	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 rankOfDiscrBdd	—	NumberField.discr_ne_zero abs_nonpos_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add Nat.cast_zero Nat.instAtLeastTwoHAddOfNat lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono one_mul lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.pi_gt_three NumberField.to_charZero lt_or_ge le_max_of_le_right Nat.le_floor_iff div_nonneg Real.log_nonneg mul_comm mul_div_assoc le_div_iff₀ div_le_iff₀ le_trans Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.one_le_cast IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass le_of_lt NumberField.abs_discr_ge Int.cast_le NeZero.charZero_one Mathlib.Tactic.Contrapose.contrapose₁ Real.rpow_natCast lt_of_le_of_lt Real.rpow_logb lt_trans zero_lt_one ne_of_gt mul_pos div_pos Nat.cast_pos' lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd mul_assoc inv_div inv_mul_cancel₀ Int.cast_natCast le_refl mul_lt_mul_of_pos_left Real.rpow_lt_rpow_of_exponent_lt Real.log_div_log le_max_of_le_left

NumberField.mixedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covolume_idealLattice 📖	mathematical	—	ZLattice.covolume mixedSpace Prod.normedAddCommGroup Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.instNormedAddCommGroup Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace Complex.measurableSpace idealLattice MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace measureSpaceOfInnerProductSpace instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace Real.instMul Real.instRatCast DFunLike.coe MonoidWithZeroHom FractionalIdeal NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring FractionalIdeal.commSemiring Rat.semiring MonoidWithZeroHom.funLike FractionalIdeal.absNorm NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instIsNoetherianInt NumberField.RingOfIntegers.instIsFractionRing Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces Real.sqrt abs Real.lattice Real.instAddGroup Real.instIntCast NumberField.discr	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain Complex.instFiniteDimensionalReal Complex.borelSpace NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Nat.instAtLeastTwoHAddOfNat NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule ZLattice.covolume_eq_measure_fundamentalDomain Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice instIsZLatticeRealMixedSpaceIdealLattice instIsAddHaarMeasureMixedSpaceVolume fundamentalDomain_idealLattice MeasureTheory.measureReal_def volume_fundamentalDomain_fractionalIdealLatticeBasis volume_fundamentalDomain_latticeBasis ENNReal.toReal_mul ENNReal.toReal_pow ENNReal.toReal_inv ENNReal.toReal_ofNat ENNReal.coe_toReal Real.coe_sqrt coe_nnnorm Int.norm_eq_abs ENNReal.toReal_ofReal Rat.cast_nonneg Real.instIsStrictOrderedRing FractionalIdeal.absNorm_nonneg mul_assoc
covolume_integerLattice 📖	mathematical	—	ZLattice.covolume mixedSpace Prod.normedAddCommGroup Pi.normedAddCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.normedAddCommGroup NumberField.InfinitePlace.IsComplex Complex Complex.instNormedAddCommGroup Prod.instMeasurableSpace MeasurableSpace.pi Real.measurableSpace Complex.measurableSpace integerLattice MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Real.measureSpace measureSpaceOfInnerProductSpace instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces Real.sqrt abs Real.lattice Real.instAddGroup Real.instIntCast NumberField.discr	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat NumberField.RingOfIntegers.instFreeInt ZLattice.covolume_eq_measure_fundamentalDomain Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice instIsZLatticeRealMixedSpaceIntegerLattice instIsAddHaarMeasureMixedSpaceVolume fundamentalDomain_integerLattice MeasureTheory.measureReal_def volume_fundamentalDomain_latticeBasis ENNReal.toReal_mul ENNReal.toReal_pow ENNReal.toReal_inv ENNReal.toReal_ofNat ENNReal.coe_toReal Real.coe_sqrt coe_nnnorm Int.norm_eq_abs
volume_fundamentalDomain_latticeBasis 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure mixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Complex measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume ZSpan.fundamentalDomain Module.Free.ChooseBasisIndex NumberField.RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing NumberField.RingOfIntegers.instFreeInt Real.normedField Prod.normedAddCommGroup Pi.normedAddCommGroup Real.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedField.toNormedCommRing Complex.instNormedField latticeBasis Real.linearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrComplexPlaces ENNReal.ofNNReal OrderIso NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Int.instNormedCommRing NumberField.discr	—	NumberField.RingOfIntegers.instFreeInt invariantBasisNumber_of_nontrivial_of_commRing Complex.instNontrivial Finite.of_fintype Complex.instCharZero NumberField.to_charZero Matrix.ext Matrix.map_apply RingHomInvPair.ids Module.Basis.toMatrix_apply Module.Basis.coe_reindex Equiv.symm_symm latticeBasis_apply commMap_canonical_eq_mixed Complex.ofRealHom_eq_coe stdBasis_repr_eq_matrixToStdBasis_mul Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat ZSpan.fundamentalDomain_reindex norm_toNNReal ZSpan.measure_fundamentalDomain Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instIsAddHaarMeasureMixedSpaceVolume volume_fundamentalDomain_stdBasis mul_one Complex.nnnorm_real RingHom.map_det RingHom.mapMatrix_apply Matrix.det_mul Matrix.det_transpose Matrix.det_reindex_self Complex.norm_I Real.toNNReal_one det_matrixToStdBasis nnnorm_mul NormedDivisionRing.toNormMulClass nnnorm_pow NormedDivisionRing.to_normOneClass nnnorm_inv ENNReal.coe_mul ENNReal.coe_pow RCLike.norm_two Real.toNNReal_ofNat ENNReal.coe_inv two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing ENNReal.coe_ofNat NNReal.sqrt_sq Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two NumberField.to_finiteDimensional Complex.isAlgClosed Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero Rat.instCharZero Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Algebra.discr_reindex NumberField.coe_discr map_intCast RingHom.instRingHomClass Complex.nnnorm_intCast

---

← Back to Index