Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.normalizedFactorsEquiv_apply

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {β : Type u_2} [inst_3 : CommMonoidWithZero β] [inst_4 : NormalizationMonoid β] [inst_5 : UniqueFactorizationMonoid β]
  {F : Type u_3} [inst_6 : EquivLike F α β] [inst_7 : MulEquivClass F α β] {f : F}
  (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a p : α}
  (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors a),
  ↑((UniqueFactorizationMonoid.normalizedFactorsEquiv he a) ⟨p, hp⟩) = f p

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizationMonoidUniqueFactorizationMonoidCommMonoidWithZeroNormalizationMonoidUniqueFactorizationMonoidEquivLikeMulEquivClass