Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `boundOfDiscBdd`, `rankOfDiscrBdd`, `rootDiscr`	3
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`, `rootDiscr_def`, `rootDiscr_rat`, `sign_discr`	21
Total	24

NumberField

Definitions

Name	Category	Theorems
`rootDiscr` 📖	CompOp	2 math math: `rootDiscr_def`, `rootDiscr_rat`

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.toPow` `Real.instMonoid` `Real.pi` `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.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.toPow` `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.instFreeInt` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `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.toPow` `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` `Mathlib.Tactic.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` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.mul_subst` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.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` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `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.toPow` `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.toPow` `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` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `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` `instCommRingRingOfIntegers` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingOfIntegers.instAlgebra_1` `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` `DivisionRing.toRing` `Field.toDivisionRing` `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` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `RingOfIntegers.instFG` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `InfinitePlace.nrComplexPlaces` `Nat.factorial` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Rat.commSemiring` `Field.toSemifield` `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` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `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	—	`RingOfIntegers` `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.toPow` `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` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `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`
`rootDiscr_def` 📖	mathematical	—	`rootDiscr` `Real` `Real.instPow` `Real.instIntCast` `abs` `instLatticeInt` `Int.instAddGroup` `discr` `Real.instInv` `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`	—	`to_charZero`
`rootDiscr_rat` 📖	mathematical	—	`rootDiscr` `Rat.instField` `Rat.numberField` `Real` `Real.instOne`	—	`Rat.numberField` `to_charZero` `rootDiscr_def` `Rat.numberField_discr` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.cast_one` `Module.finrank_self` `commRing_strongRankCondition` `Rat.nontrivial` `Nat.cast_one` `inv_one` `Real.rpow_one`
`sign_discr` 📖	mathematical	—	`discr` `Monoid.toPow` `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` `zero_le` `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` `zero_le` `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` `IntermediateField` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing`	—	`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.instCommRingRingOfIntegers` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers.instAlgebra_1` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instIsDedekindDomain` `Units.instOne` `ENNReal.ofNNReal` `boundOfDiscBdd`	—	`add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `NNReal.addLeftReflectLT` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `lt_of_le_of_lt` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instIsDedekindDomain` `Complex.instFiniteDimensionalReal` `Complex.borelSpace` `NumberField.mixedEmbedding.minkowskiBound.eq_1` `NumberField.RingOfIntegers.instFreeInt` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `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` `Field.toDivisionRing` `Ring.toIntAlgebra` `NumberField.RingOfIntegers.val` `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` `Mathlib.Tactic.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` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.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.instCommRingRingOfIntegers` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FractionalIdeal.commSemiring` `Rat.semiring` `MonoidWithZeroHom.funLike` `FractionalIdeal.absNorm` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instFreeInt` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instIsFractionRing` `Units.val` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `Monoid.toPow` `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` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `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.toPow` `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.instCommRingRingOfIntegers` `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.toPow` `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` `NNReal.instPartialOrder` `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` `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` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `Algebra.discr_reindex` `NumberField.coe_discr` `map_intCast` `RingHom.instRingHomClass` `Complex.nnnorm_intCast`

---

← Back to Index