GaussLemma

📁 Source: Mathlib/RingTheory/DedekindDomain/GaussLemma.lean

Statistics

Metric	Count
Definitions	0
Theorems contentIdeal_eq_top_iff_forall_gaussNorm_eq_one, gaussNorm_intAdicAbv_le_one, gaussNorm_lt_one_iff_contentIdeal_le, isPrimitive_iff_forall_gaussNorm_eq_one	4
Total	4

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contentIdeal_eq_top_iff_forall_gaussNorm_eq_one 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal IsField CommSemiring.toSemiring CommRing.toCommSemiring	contentIdeal Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule gaussNorm AbsoluteValue Real Real.semiring Real.partialOrder AbsoluteValue.funLike IsDedekindDomain.HeightOneSpectrum.intAdicAbv Real.instOne	—	IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists
gaussNorm_intAdicAbv_le_one 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLE gaussNorm AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike IsDedekindDomain.HeightOneSpectrum.intAdicAbv Real.instOne	—	gaussNorm_zero Real.instZeroLEOneClass Finset.sup'_congr one_pow mul_one
gaussNorm_lt_one_iff_contentIdeal_le 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLT gaussNorm AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike IsDedekindDomain.HeightOneSpectrum.intAdicAbv Real.instOne Ideal Preorder.toLE Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule contentIdeal IsDedekindDomain.HeightOneSpectrum.asIdeal	—	gaussNorm_zero Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing contentIdeal_zero Finset.sup'_congr one_pow mul_one IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Finset.le_sup'_of_le Finset.sup'_lt_iff coeff_mem_coeffs mem_support_iff
isPrimitive_iff_forall_gaussNorm_eq_one 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	IsPrimitive gaussNorm AbsoluteValue Real Real.semiring Real.partialOrder AbsoluteValue.funLike IsDedekindDomain.HeightOneSpectrum.intAdicAbv IsPrincipalIdealRing.isDedekindDomain Real.instOne	—	IsPrincipalIdealRing.isDedekindDomain isPrimitive_iff_contentIdeal_eq_top IsBezout.of_isPrincipalIdealRing contentIdeal_eq_top_iff_forall_gaussNorm_eq_one

---

← Back to Index