Int

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

Statistics

Metric	Count
Definitions	0
Theorems ringChar_quot, absNorm_under_dvd_absNorm, absNorm_under_eq_sInf, absNorm_under_mem, cast_mem_ideal_iff, ideal_span_isMaximal_of_prime, liesOver_span_absNorm, absNorm_under_prime	8
Total	8

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringChar_quot 📖	mathematical	—	ringChar HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 Semiring.toNonAssocSemiring Quotient.semiring DFunLike.coe MonoidWithZeroHom Int.instCommRing NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Int.instNontrivial IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Int.euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg Int.instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree under Int.instCommSemiring Ring.toIntAlgebra	—	Int.instNontrivial IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree ringChar.eq_iff charP_iff instIsTwoSided_1 Quotient.eq_zero_iff_mem Int.cast_natCast Int.cast_mem_ideal_iff

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absNorm_under_dvd_absNorm 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.under instCommSemiring Ring.toIntAlgebra IsDomain.toNontrivial IsDedekindDomain.toIsDomain	—	finite_or_infinite instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree IsDomain.toNontrivial IsDedekindDomain.toIsDomain nsmul_eq_mul Ideal.instIsTwoSided_1 map_natCast RingHom.instRingHomClass MulZeroClass.zero_mul mul_one Ideal.absNorm_apply Submodule.cardQuot_apply Nat.card_eq_fintype_card absNorm_under_eq_sInf AddGroup.exponent_dvd_card Nat.card_eq_zero_of_infinite
absNorm_under_eq_sInf 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.under instCommSemiring Ring.toSemiring Ring.toIntAlgebra InfSet.sInf Nat.instInfSet setOf SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Set.eq_empty_of_forall_notMem cast_mem_ideal_iff cast_natCast Nat.sInf_empty absNorm_under_mem le_antisymm Nat.sInf_mem Set.nonempty_of_mem lt_iff_not_ge Nat.sInf_le
absNorm_under_mem 📖	mathematical	—	Ideal Ring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe MonoidWithZeroHom CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.under instCommSemiring Ring.toIntAlgebra	—	instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree cast_natCast cast_mem_ideal_iff dvd_refl
cast_mem_ideal_iff 📖	mathematical	—	Ideal Ring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DFunLike.coe MonoidWithZeroHom CommSemiring.toSemiring CommRing.toCommSemiring instCommRing NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.under instCommSemiring Ring.toIntAlgebra	—	instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.mem_span_singleton ideal_span_absNorm_eq_self RingHom.instRingHomClass Ideal.under_def Ideal.mem_comap eq_intCast
ideal_span_isMaximal_of_prime 📖	mathematical	—	Ideal.IsMaximal instSemiring Ideal.span Set Set.instSingletonSet	—	Ideal.Quotient.maximal_of_isField MulEquiv.isField Field.toIsField
liesOver_span_absNorm 📖	mathematical	—	Ideal.LiesOver instCommSemiring Ring.toSemiring Ring.toIntAlgebra Ideal.span CommSemiring.toSemiring Set Set.instSingletonSet DFunLike.coe MonoidWithZeroHom Ideal CommRing.toCommSemiring instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.under	—	instNontrivial IsPrincipalIdealRing.isDedekindDomain instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree Ideal.liesOver_iff RingHom.instRingHomClass Ideal.under_def ideal_span_absNorm_eq_self

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absNorm_under_prime 📖	mathematical	—	Prime DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm Int.instNontrivial IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Int.euclideanDomain Module.free_of_finite_type_torsion_free' Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg Int.instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree Ideal.under Int.instCommSemiring Ring.toIntAlgebra	—	Int.instNontrivial IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Module.free_of_finite_type_torsion_free' AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsAddTorsionFree prime_iff_prime_int Ideal.span_singleton_prime Iff.not Ideal.absNorm_eq_zero_iff Mathlib.Tactic.Contrapose.contrapose₄ Ideal.eq_bot_of_comap_eq_bot Int.ideal_span_absNorm_eq_self Ideal.IsPrime.under

---

← Back to Index