AbsNorm

📁 Source: Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

Statistics

Metric	Count
Definitions absNorm, cardQuot	2
Theorems absNorm_apply, absNorm_bot, absNorm_dvd_absNorm_of_le, absNorm_dvd_norm_of_mem, absNorm_eq_one_iff, absNorm_eq_zero_iff, absNorm_mem, absNorm_ne_zero_iff, absNorm_ne_zero_iff_mem_nonZeroDivisors, absNorm_ne_zero_of_nonZeroDivisors, absNorm_pos_iff_mem_nonZeroDivisors, absNorm_pos_of_nonZeroDivisors, absNorm_span_insert, absNorm_span_singleton, absNorm_top, card_norm_le_eq_card_norm_le_add_one, exists_mul_add_mem_pow_succ, finite_setOf_absNorm_eq, finite_setOf_absNorm_le, finite_setOf_absNorm_le₀, irreducible_of_irreducible_absNorm, isPrime_of_irreducible_absNorm, mem_prime_of_mul_mem_pow, mul_add_mem_pow_succ_inj, mul_add_mem_pow_succ_unique, natAbs_det_basis_change, natAbs_det_equiv, norm_dvd_iff, prime_of_irreducible_absNorm_span, span_singleton_absNorm, span_singleton_absNorm_le, ideal_span_absNorm_eq_self, cardQuot_apply, cardQuot_bot, cardQuot_eq_one_iff, cardQuot_top, cardQuot_mul, cardQuot_mul_of_coprime, cardQuot_pow_of_prime	39
Total	41

Ideal

Definitions

Name	Category	Theorems
absNorm 📖	CompOp	69 math math: finite_setOf_absNorm_le₀, absNorm_span_insert, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, NumberField.FinitePlace.norm_def', finite_setOf_absNorm_eq, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, NumberField.HeightOneSpectrum.rankOne_hom'_def, FractionalIdeal.absNorm_eq', absNorm_pos_iff_mem_nonZeroDivisors, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, absNorm_eq_pow_inertiaDeg', NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, absNorm_eq_pow_inertiaDeg_of_liesOver, absNorm_mem, NumberField.HeightOneSpectrum.adicAbv_def, Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Ring.HasFiniteQuotients.finite_absNorm_le, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, relNorm_int, absNorm_dvd_absNorm_of_le, NumberField.Ideal.tendsto_norm_le_div_atTop₀, NumberField.HeightOneSpectrum.embedding_mul_absNorm, Int.absNorm_under_mem, FractionalIdeal.absNorm_eq, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, NumberField.FinitePlace.norm_def_int, card_norm_le_eq_card_norm_le_add_one, NumberField.absNorm_differentIdeal, absNorm_top, absNorm_apply, absNorm_pos_of_nonZeroDivisors, Int.absNorm_under_dvd_absNorm, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, NumberField.exists_ideal_in_class_of_norm_le, NumberField.Ideal.tendsto_norm_le_div_atTop, natAbs_det_equiv, absNorm_eq_one_iff, NumberField.torsionOrder_dvd_absNorm_sub_one, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, finite_setOf_absNorm_le, span_singleton_absNorm, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, absNorm_eq_pow_inertiaDeg, NumberField.HeightOneSpectrum.one_lt_absNorm, absNorm_eq_zero_iff, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, absNorm_bot, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, Int.ideal_span_absNorm_eq_self, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', absNorm_relNorm, Int.absNorm_under_eq_sInf, absNorm_span_singleton, FractionalIdeal.coeIdeal_absNorm, absNorm_algebraMap, Int.cast_mem_ideal_iff, span_singleton_absNorm_le, natAbs_det_basis_change, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, ringChar_quot, Int.liesOver_span_absNorm, NumberField.FinitePlace.norm_embedding_int, Nat.absNorm_under_prime, NumberField.FinitePlace.norm_def, absNorm_dvd_norm_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absNorm_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Submodule.cardQuot CommRing.toRing Ring.toAddCommGroup Semiring.toModule	—	—
absNorm_bot 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	zero_eq_bot map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
absNorm_dvd_absNorm_of_le 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	map_dvd IsScalarTower.right MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass dvd_iff_le
absNorm_dvd_norm_of_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Ring.toSemiring CommRing.toRing Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra	—	absNorm_span_singleton absNorm_dvd_absNorm_of_le span_singleton_le_iff_mem
absNorm_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Top.top Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	absNorm_apply Submodule.cardQuot_eq_one_iff
absNorm_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	le_bot_iff mem_bot Algebra.norm_eq_zero_iff Int.instIsDomain IsDedekindDomain.toIsDomain absNorm_span_singleton zero_dvd_iff absNorm_dvd_absNorm_of_le span_singleton_le_iff_mem absNorm_bot
absNorm_mem 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	absNorm_apply Submodule.cardQuot.eq_1 instIsTwoSided_1 Quotient.eq_zero_iff_mem map_natCast RingHom.instRingHomClass Quotient.index_eq_zero
absNorm_ne_zero_iff 📖	mathematical	—	Finite HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1	—	Nat.finite_of_card_ne_zero AddSubgroup.FiniteIndex.index_ne_zero AddSubgroup.finiteIndex_of_finite_quotient
absNorm_ne_zero_iff_mem_nonZeroDivisors 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	instNoZeroDivisors IsDomain.to_noZeroDivisors IsDedekindDomain.toIsDomain instNontrivial
absNorm_ne_zero_of_nonZeroDivisors 📖	—	—	—	—	absNorm_ne_zero_iff_mem_nonZeroDivisors SetLike.coe_mem
absNorm_pos_iff_mem_nonZeroDivisors 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	absNorm_ne_zero_iff_mem_nonZeroDivisors
absNorm_pos_of_nonZeroDivisors 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	absNorm_pos_iff_mem_nonZeroDivisors SetLike.coe_mem
absNorm_span_insert 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm span Set Set.instInsert GCDMonoid.gcd Nat.instCommMonoidWithZero instGCDMonoidNat MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Ring.toSemiring CommRing.toRing Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra	—	dvd_gcd_iff absNorm_dvd_absNorm_of_le span_mono Set.subset_insert trans instIsTransDvd Set.singleton_subset_iff Set.mem_insert absNorm_span_singleton dvd_refl
absNorm_span_singleton 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm span Set Set.instSingletonSet MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Ring.toSemiring CommRing.toRing Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra	—	smulCommClass_self IsScalarTower.left Algebra.norm_apply span_zero absNorm_bot map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass LinearMap.det_zero'' RingHomCompTriple.ids LinearMap.CompatibleSMul.intModule RingHomInvPair.ids IsScalarTower.right AddEquivClass.instAddMonoidHomClass SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass IsDedekindDomain.toIsDomain natAbs_det_equiv Module.Basis.ext Module.Basis.equiv_apply basisSpanSingleton_apply
absNorm_top 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Top.top Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	one_eq_top map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
card_norm_le_eq_card_norm_le_add_one 📖	mathematical	—	Nat.card Ideal CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	Set.Finite.subset finite_setOf_absNorm_le Nat.card_congr Pi.disjoint_iff Prop.disjoint_iff Nat.card_sum instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid absNorm_ne_zero_iff_mem_nonZeroDivisors absNorm_eq_zero_iff Nat.card_unique Unique.instSubsingleton
exists_mul_add_mem_pow_succ 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul	—	IsScalarTower.right eq_prime_pow_of_succ_lt_of_le lt_of_le_of_ne le_sup_right Mathlib.Tactic.Contrapose.contrapose₄ Submodule.mem_sup mem_span_singleton_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass add_zero sup_le span_le Set.singleton_subset_iff LT.lt.le pow_succ_lt_pow mul_comm mem_span_singleton_sup
finite_setOf_absNorm_eq 📖	mathematical	—	Set.Finite Ideal CommSemiring.toSemiring CommRing.toCommSemiring setOf DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	instIsTwoSided_1 Set.Finite.of_finite_image absNorm_ne_zero_iff absNorm_span_singleton Int.instIsDomain IsDedekindDomain.toIsDomain ne_of_gt Set.Finite.subset Set.finite_univ Set.instFinite Set.subset_univ Function.Injective.injOn SetLike.coe_injective RingHom.instRingHomClass span_singleton_absNorm_le
finite_setOf_absNorm_le 📖	mathematical	—	Set.Finite Ideal CommSemiring.toSemiring CommRing.toCommSemiring setOf DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	Set.ext Set.iUnion_congr_Prop Nat.instCanonicallyOrderedAdd Set.Finite.biUnion Set.finite_Icc finite_setOf_absNorm_eq
finite_setOf_absNorm_le₀ 📖	mathematical	—	Set.Finite Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors setOf DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	Set.Finite.subset finite_setOf_absNorm_le Finite.of_equiv
irreducible_of_irreducible_absNorm 📖	mathematical	Irreducible Nat.instMonoid DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	Irreducible Ideal CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	—	irreducible_iff Irreducible.not_isUnit Irreducible.isUnit_or_isUnit map_mul IsScalarTower.right MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
isPrime_of_irreducible_absNorm 📖	mathematical	Irreducible Nat.instMonoid DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	IsPrime CommSemiring.toSemiring CommRing.toCommSemiring	—	isPrime_of_prime UniqueFactorizationMonoid.irreducible_iff_prime uniqueFactorizationMonoid irreducible_of_irreducible_absNorm
mem_prime_of_mul_mem_pow 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsScalarTower.right prime_pow_succ_dvd_mul isCancelMulZero prime_of_isPrime IsScalarTower.left pow_succ instIsTwoSided_1
mul_add_mem_pow_succ_inj 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul	—	IsScalarTower.right mul_mem_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr 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 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_gt add_mem sub_mem
mul_add_mem_pow_succ_unique 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	IsScalarTower.right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add add_mem sub_mem mem_prime_of_mul_mem_pow
natAbs_det_basis_change 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.Basis Int.instSemiring Submodule.addCommMonoid Submodule.addCommGroup Module.Basis.instFunLike MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	Submodule.natAbs_det_basis_change IsScalarTower.right
natAbs_det_equiv 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddCommGroup.toIntModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearMap.comp Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.addCommGroup RingHomCompTriple.ids LinearMap.restrictScalars Int.instSemiring Submodule.module LinearMap.CompatibleSMul.intModule Submodule.subtype AddMonoidHom.toIntLinearMap AddMonoidHomClass.toAddMonoidHom Ideal AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup EquivLike.toFunLike AddEquivClass.instAddMonoidHomClass MonoidWithZeroHom IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	RingHomCompTriple.ids LinearMap.CompatibleSMul.intModule AddEquivClass.instAddMonoidHomClass one_ne_zero NeZero.one EquivLike.injective Unique.instSubsingleton Submodule.natAbs_det_equiv IsScalarTower.right
norm_dvd_iff 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero Int.instCommSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MonoidHom.instFunLike Algebra.norm Ring.toIntAlgebra semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	mem_span_singleton eq_intCast RingHom.instRingHomClass mem_comap span_singleton_absNorm absNorm_span_singleton Int.prime_iff_natAbs_prime
prime_of_irreducible_absNorm_span 📖	mathematical	Irreducible Nat.instMonoid DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm span Set Set.instSingletonSet	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	—	span_singleton_prime isPrime_of_irreducible_absNorm
span_singleton_absNorm 📖	mathematical	Nat.Prime DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	span Int.instSemiring Set Set.instSingletonSet DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm comap RingHom Int.instCommSemiring RingHom.instFunLike algebraMap Ring.toIntAlgebra CommRing.toRing RingHom.instRingHomClass	—	span_singleton_prime Nat.Prime.ne_zero Nat.prime_iff_prime_int IsMaximal.eq_of_le RingHom.instRingHomClass IsPrime.isMaximal IsDedekindDomainDvr.ring_dimensionLEOne Int.instIsDomain IsDedekindDomain.isDedekindDomainDvr IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain span_singleton_eq_bot IsPrime.ne_top IsPrime.comap isPrime_of_irreducible_absNorm Nat.irreducible_iff_nat_prime span_singleton_le_iff_mem mem_comap algebraMap_int_eq map_natCast absNorm_mem
span_singleton_absNorm_le 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm	—	absNorm_mem

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ideal_span_absNorm_eq_self 📖	mathematical	—	Ideal.span instSemiring Set Set.instSingletonSet 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' instAddCommGroup AddCommGroup.toIntModule Ring.toAddCommGroup CommRing.toRing AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg instAddGroup AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree instIsAddTorsionFree	—	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 IsPrincipalIdealRing.principal Ideal.absNorm_span_singleton Algebra.norm_self Nat.cast_natAbs cast_abs instIsStrictOrderedRing Ideal.span_singleton_abs

Submodule

Definitions

Name	Category	Theorems
cardQuot 📖	CompOp	11 math math: cardQuot_mul, Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le, cardQuot_pow_of_prime, Ring.HasFiniteQuotients.cardQuot_pos, Ideal.absNorm_apply, Ring.HasFiniteQuotients.finite_cardQuot_le, cardQuot_eq_one_iff, cardQuot_bot, cardQuot_top, cardQuot_mul_of_coprime, cardQuot_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardQuot_apply 📖	mathematical	—	cardQuot Nat.card HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient	—	—
cardQuot_bot 📖	mathematical	—	cardQuot Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instBot	—	AddSubgroup.index_bot Nat.card_eq_zero_of_infinite
cardQuot_eq_one_iff 📖	mathematical	—	cardQuot Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instTop	—	AddSubgroup.index_eq_one neg_mem
cardQuot_top 📖	mathematical	—	cardQuot Top.top Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instTop	—	AddSubgroup.index_top

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardQuot_mul 📖	mathematical	—	Submodule.cardQuot CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.mul IsScalarTower.right Algebra.id	—	UniqueFactorizationMonoid.multiplicative_of_coprime Ideal.uniqueFactorizationMonoid Submodule.cardQuot_bot Infinite.of_surjective Finsupp.infinite_of_right Int.infinite Module.Free.instNonemptyChooseBasisIndexOfNontrivial IsDomain.toNontrivial IsDedekindDomain.toIsDomain RingHomInvPair.ids Equiv.surjective Ideal.isUnit_iff Ideal.mul_top Ideal.instIsTwoSided_1 Submodule.cardQuot_top mul_one Ideal.isPrime_of_prime cardQuot_pow_of_prime Prime.ne_zero cardQuot_mul_of_coprime Ideal.isCoprime_iff_sup_eq IsScalarTower.right Ideal.dvd_iff_le le_sup_left le_sup_right
cardQuot_mul_of_coprime 📖	mathematical	IsCoprime Ideal CommSemiring.toSemiring CommRing.toCommSemiring IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring	Submodule.cardQuot CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.mul IsScalarTower.right Algebra.id	—	IsScalarTower.right Submodule.cardQuot_apply Nat.card_congr Nat.card_prod
cardQuot_pow_of_prime 📖	mathematical	—	Submodule.cardQuot CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id Monoid.toPow Nat.instMonoid	—	IsScalarTower.right pow_zero Ideal.one_eq_top Submodule.cardQuot_top Ideal.pow_succ_lt_pow RingHomSurjective.ids Subtype.prop Submodule.mkQ_apply Submodule.Quotient.eq Submodule.mem_map Ideal.mul_mem_right Ideal.instIsTwoSided_1 Ideal.mul_add_mem_pow_succ_unique ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass add_zero Ideal.exists_mul_add_mem_pow_succ SetLike.exists_of_lt instIsConcreteLE pow_succ' Submodule.cardQuot_apply Submodule.card_quotient_mul_card_quotient LT.lt.le Nat.card_congr

---

← Back to Index