Theorems · Theorem · commutative algebra
Ideal.absNorm_pos_of_nonZeroDivisors
∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
(I : ↥(nonZeroDivisors (Ideal S))), 0 < Ideal.absNorm ↑I- Defined in
- Mathlib.RingTheory.Ideal.Norm.AbsNorm
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Idealstatement and proof · cited by 4,748
- Submonoidstatement · cited by 3,086
- Module.Finitestatement and proof · cited by 1,032
- nonZeroDivisorsstatement and proof · cited by 895
- MonoidWithZeroHomstatement · cited by 704
- IsDedekindDomainstatement and proof · cited by 668
- Module.Freestatement and proof · cited by 597
- Ideal.absNormstatement · cited by 123
- SetLike.coe_memproof · cited by 46
- Ideal.absNorm_pos_iff_mem_nonZeroDivisorsproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTopproof · cited by 1
- RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrimeproof · cited by 1