Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity

∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {α : Type u_3} {M : Type u_4}
  [inst_2 : CommMonoid M] [Subsingleton Rˣ] (f : α → M) {g : α → R},
  Function.Injective g →
    (∀ (s : α), Irreducible (g s)) → ∀ {r : R}, r ≠ 0 → Function.HasFiniteMulSupport fun s => f s ^ multiplicity (g s) r

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidCommMonoidSubsingleton