Theorems · Theorem · number theory

FractionalIdeal.absNorm_eq_zero_iff

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [IsDomain K] {I : FractionalIdeal (nonZeroDivisors R) K}, FractionalIdeal.absNorm I = 0 ↔ I = 0

Defined in: Mathlib.RingTheory.FractionalIdeal.Norm
Cited by: 0 results in Mathlib
Foundations: Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDedekindDomain Module.Free Module.Finite CommRing Algebra IsFractionRing IsDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
IsDomainstatement and proof · cited by 2,196
Module.Finitestatement and proof · cited by 1,032
nonZeroDivisorsstatement and proof · cited by 895
IsFractionRingstatement and proof · cited by 738
MonoidWithZeroHomstatement · cited by 704
IsDedekindDomainstatement and proof · cited by 668
Module.Freestatement and proof · cited by 597
FractionalIdealstatement and proof · cited by 423
Int.cast_absproof · cited by 54

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.