Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x y : α},
  x ≠ 0 →
    y ≠ 0 →
      (DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y)

Defined in: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Cited by: 1 results in Mathlib
Foundations: Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommMonoidWithZero NormalizationMonoid UniqueFactorizationMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

Multisetstatement · cited by 2,627
LT.lt.leproof · cited by 2,189
IsUnitproof · cited by 1,602
CommMonoidWithZerostatement and proof · cited by 913
LT.lt.not_geproof · cited by 305
UniqueFactorizationMonoidstatement and proof · cited by 279
NormalizationMonoidstatement and proof · cited by 165
UniqueFactorizationMonoid.normalizedFactorsstatement and proof · cited by 151
right_ne_zero_of_mulproof · cited by 38
DvdNotUnitstatement and proof · cited by 33
UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactorsproof · cited by 11
UniqueFactorizationMonoid.normalizedFactors_mulproof · cited by 11

Cited by1

Results whose statement or proof uses this declaration.

Ideal.eq_prime_pow_of_succ_lt_of_leproof · cited by 1