Defs

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

Statistics

Metric	Count
Definitions discr	1
Theorems discr_eq_discr_of_toMatrix_coeff_isIntegral, coe_discr, discr_eq_discr, discr_eq_discr_of_algEquiv, discr_eq_discr_of_ringEquiv, discr_ne_zero, discr_rat, numberField_discr	8
Total	9

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discr_eq_discr_of_toMatrix_coeff_isIntegral 📖	mathematical	IsIntegral Int.instCommRing DivisionRing.toRing Rat.instDivisionRing Ring.toIntAlgebra Module.Basis.toMatrix Rat.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero DFunLike.coe Module.Basis Rat.semiring Module.Basis.instFunLike	discr Rat.commRing	—	NumberField.to_charZero invariantBasisNumber_of_nontrivial_of_commRing Rat.nontrivial RingHomInvPair.ids Module.Basis.coe_reindex Module.Basis.toMatrix_map_vecMul discr_of_matrix_vecMul one_mul discr_reindex IsIntegral.det IsIntegrallyClosed.isIntegral_iff Rat.isFractionRing IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain isUnit_iff_exists_inv instIsDedekindFiniteMonoid map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Matrix.det_mul Module.Basis.toMatrix_mul_toMatrix_flip Matrix.det_one IsFractionRing.injective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Int.isUnit_iff eq_intCast Int.cast_one one_pow Int.cast_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat

NumberField

Definitions

Name	Category	Theorems
discr 📖	CompOp	39 math math: discr_eq_discr_of_ringEquiv, dedekindZeta_residue_def, natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, abs_discr_ge', abs_discr_ge, discr_rat, IsCyclotomicExtension.Rat.absdiscr_prime_pow, natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, abs_discr_gt_two, IsCyclotomicExtension.Rat.discr, hermiteTheorem.finite_of_discr_bdd_of_isComplex, mixedEmbedding.covolume_idealLattice, discr_eq_discr, IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ, Ideal.tendsto_norm_le_div_atTop₀, IsCyclotomicExtension.Rat.discr_prime_pow_succ, discr_eq_basisMatrix_det_sq, mixedEmbedding.covolume_integerLattice, discr_mem_differentIdeal, absNorm_differentIdeal, IsCyclotomicExtension.Rat.natAbs_discr, finite_of_discr_bdd, IsCyclotomicExtension.Rat.absdiscr_prime, IsCyclotomicExtension.Rat.discr_prime_pow, exists_ideal_in_class_of_norm_le, Ideal.tendsto_norm_le_div_atTop, exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, discr_dvd_discr, abs_discr_ge_of_isTotallyComplex, sign_discr, mixedEmbedding.volume_fundamentalDomain_latticeBasis, abs_discr_rpow_ge_of_isTotallyComplex, exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, discr_eq_discr_of_algEquiv, Ideal.tendsto_norm_le_and_mk_eq_div_atTop, coe_discr, IsCyclotomicExtension.Rat.discr_prime, Rat.numberField_discr, hermiteTheorem.finite_of_discr_bdd_of_isReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_discr 📖	mathematical	—	discr Algebra.discr Module.Free.ChooseBasisIndex RingOfIntegers Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingOfIntegers.instCommRing AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing RingOfIntegers.instFreeInt Module.Free.instDecidableEqChooseBasisIndex Rat.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero Module.Free.ChooseBasisIndex.fintype Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt DFunLike.coe Module.Basis Rat.semiring Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.Basis.instFunLike integralBasis	—	RingOfIntegers.instFreeInt to_charZero Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt Rat.isFractionRing AddCommGroup.intIsScalarTower RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors Algebra.discr_localizationLocalization
discr_eq_discr 📖	mathematical	—	Algebra.discr RingOfIntegers Int.instCommRing RingOfIntegers.instCommRing Ring.toIntAlgebra CommRing.toRing DFunLike.coe Module.Basis Int.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toIntModule Ring.toAddCommGroup Module.Basis.instFunLike discr	—	RingOfIntegers.instFreeInt invariantBasisNumber_of_nontrivial_of_commRing Int.instNontrivial Algebra.discr_eq_discr Module.Basis.coe_reindex Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt Algebra.discr_reindex
discr_eq_discr_of_algEquiv 📖	mathematical	—	discr	—	to_charZero RingHomInvPair.ids AddCommGroup.intIsScalarTower RingOfIntegers.instFreeInt Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt coe_discr Algebra.discr_eq_discr_of_algEquiv discr_eq_discr Rat.isFractionRing RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors Algebra.discr_localizationLocalization integralBasis_apply Module.Basis.localizationLocalization_apply
discr_eq_discr_of_ringEquiv 📖	mathematical	—	discr	—	discr_eq_discr_of_algEquiv to_charZero eq_ratCast RingHom.instRingHomClass map_ratCast RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
discr_ne_zero 📖	—	—	—	—	Int.cast_injective Rat.instCharZero RingOfIntegers.instFreeInt to_charZero Module.IsNoetherian.finite RingOfIntegers.instIsNoetherianInt coe_discr Algebra.discr_not_zero_of_basis to_finiteDimensional Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsAlgebraic.of_finite Rat.nontrivial PerfectField.ofCharZero
discr_rat 📖	mathematical	—	discr Rat.instField Rat.numberField	—	Rat.numberField_discr

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
numberField_discr 📖	mathematical	—	NumberField.discr instField numberField	—	RingHomInvPair.ids numberField NumberField.discr_eq_discr Algebra.discr_def Matrix.det_unique Algebra.traceMatrix_apply Algebra.traceForm_apply Module.Basis.map_apply RingEquivClass.toAddEquivClass RingEquiv.instRingEquivClass RingEquiv.toAddEquiv_eq_coe AddEquiv.toIntLinearEquiv_symm AddEquiv.coe_toIntLinearEquiv Module.Basis.singleton_apply map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass mul_one Algebra.trace_eq_matrix_trace AlgHomClass.toRingHomClass AlgHom.algHomClass Matrix.trace_one Fintype.card_unique Nat.cast_one

---

← Back to Index