NatInt

📁 Source: Mathlib/RingTheory/Ideal/NatInt.lean

Statistics

Metric	Count
Definitions	0
Theorems isPrime_int_iff, isPrime_nat_iff, map_comap_natCastRingHom_int, coe_maximalIdeal, maximalIdeal_eq_span_two_three, mem_maximalIdeal_iff, one_mem_closure_iff, one_mem_span_iff, instIsLocalRingNat, ringKrullDim_nat	10
Total	10

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_int_iff 📖	mathematical	—	IsPrime Int.instSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Nat.Prime span Set Set.instSingletonSet	—	isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors EuclideanDomain.to_principal_ideal_domain IsDomain.to_noZeroDivisors Int.instIsDomain Int.instNontrivial Int.prime_iff_natAbs_prime Int.span_natAbs Nat.prime_iff_prime_int
isPrime_nat_iff 📖	mathematical	—	IsPrime Nat.instSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal Nat.instCommSemiring instIsLocalRingNat Nat.Prime span Set Set.instSingletonSet	—	instIsLocalRingNat isPrime_bot Nat.instNontrivial IsDomain.to_noZeroDivisors Nat.instIsDomain IsMaximal.isPrime IsLocalRing.maximalIdeal.isMaximal span_singleton_prime Nat.Prime.ne_zero Nat.prime_iff LE.le.antisymm IsLocalRing.le_maximalIdeal IsPrime.ne_top SetLike.not_le_iff_exists instIsConcreteLE le_bot_iff Nat.find_spec one_notMem Nat.prime_iff_not_exists_mul_eq mul_ne_zero_iff IsPrime.mem_or_mem Nat.find_min SetLike.exists_of_lt LE.le.lt_of_ne span_singleton_le_iff_mem Mathlib.Tactic.Push.not_and_eq eq_or_ne zero_mem Nat.mem_maximalIdeal_iff Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le Nat.Prime.coprime_iff_not_dvd Iff.not mem_span_singleton Unique.instSubsingleton LT.lt.le IsPrime.mem_of_pow_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass mul_mem_left
map_comap_natCastRingHom_int 📖	mathematical	—	map RingHom Nat.instNonAssocSemiring Semiring.toNonAssocSemiring Int.instSemiring Nat.instSemiring RingHom.instFunLike Nat.castRingHom comap RingHom.instRingHomClass	—	LE.le.antisymm RingHom.instRingHomClass map_comap_le mul_mem_left mem_map_of_mem mem_comap

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_maximalIdeal 📖	mathematical	—	SetLike.coe Ideal CommSemiring.toSemiring instCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRingNat Compl.compl Set Set.instCompl Set.instSingletonSet	—	Set.ext instIsLocalRingNat Unique.instSubsingleton
maximalIdeal_eq_span_two_three 📖	mathematical	—	IsLocalRing.maximalIdeal instCommSemiring instIsLocalRingNat Ideal.span CommSemiring.toSemiring Set Set.instInsert Set.instSingletonSet	—	le_antisymm instIsLocalRingNat Ne.lt_or_gt mem_maximalIdeal_iff ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Ideal.mem_span_pair exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le Unique.instSubsingleton Ideal.span_le Set.pair_subset instCharZero instAtLeastTwoHAddOfNat
mem_maximalIdeal_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring instCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRingNat	—	instIsLocalRingNat Unique.instSubsingleton
one_mem_closure_iff 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass instAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure Set Set.instMembership	—	Submodule.span_nat_eq_addSubmonoidClosure one_mem_span_iff
one_mem_span_iff 📖	mathematical	—	Ideal instSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instMembership	—	SetLike.mem_coe not_iff_not instIsLocalRingNat instIsConcreteLE

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalRingNat 📖	mathematical	—	IsLocalRing Nat.instSemiring	—	Nat.instNontrivial Unique.instSubsingleton
ringKrullDim_nat 📖	mathematical	—	ringKrullDim Nat.instCommSemiring WithBot ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	—	le_antisymm Nat.instAtLeastTwoHAddOfNat iSup_le le_of_not_gt ENat.coe_lt_coe WithBot.coe_lt_coe three_ne_zero LE.le.trans_lt bot_le RelSeries.step instIsLocalRingNat Ideal.isPrime_nat_iff PrimeSpectrum.isPrime LT.lt.ne' LE.le.not_gt IsLocalRing.le_maximalIdeal_of_isPrime Eq.trans_lt LT.lt.trans Irreducible.not_isUnit DvdNotUnit.isUnit_of_irreducible_right Ideal.span_singleton_lt_span_singleton Nat.instIsDomain LT.lt.trans_eq le_iSup_of_le Ideal.span_singleton_prime two_ne_zero Nat.prime_iff Nat.prime_two Ideal.IsMaximal.isPrime IsLocalRing.maximalIdeal.isMaximal Fintype.complete bot_lt_iff_ne_bot Iff.not Ideal.span_singleton_eq_bot Nat.maximalIdeal_eq_span_two_three SetLike.lt_iff_le_and_exists instIsConcreteLE Ideal.span_mono Ideal.subset_span Ideal.mem_span_singleton le_rfl

---

← Back to Index