Theorems · Theorem · commutative algebra

emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso

∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N},
  n ≠ 0 →
    ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)),
      emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

Defined in: Mathlib.RingTheory.ChainOfDivisors
Cited by: 1 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommMonoidWithZero IsCancelMulZero CommMonoidWithZero UniqueFactorizationMonoid UniqueFactorizationMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites22

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
Setstatement · cited by 53,352
Set.Elemstatement and proof · cited by 7,166
ENatstatement · cited by 4,985
Unitsstatement · cited by 2,804
Multisetstatement · cited by 2,627
le_antisymmproof · cited by 2,068
Set.Iicstatement and proof · cited by 1,111
CommMonoidWithZerostatement and proof · cited by 913
OrderIsostatement and proof · cited by 874
OrderIso.symmproof · cited by 475
UniqueFactorizationMonoidstatement and proof · cited by 279

Cited by1

Results whose statement or proof uses this declaration.

emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactorsproof · cited by 1