factors_eq_normalizedFactors — Mathlib

English

If a ≠ 0 and p is irreducible and p ∣ a, then there exists q ∈ normalizedFactors a with p associated to q.

Русский

Если a ≠ 0 и p неразложимо и p делит a, то найдётся q в normalizedFactors a такое, что p ассоциировано с q.

LaTeX

$$$p \mid a \to \exists q \in normalizedFactors(a), p \sim_u q$$$

Lean4

/-- An arbitrary choice of factors of `x : M` is exactly the (unique) normalized set of factors,
if `M` has a trivial group of units. -/
@[simp]
theorem factors_eq_normalizedFactors {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M]
    [Subsingleton Mˣ] (x : M) : factors x = normalizedFactors x :=
  by
  unfold normalizedFactors
  convert (Multiset.map_id (factors x)).symm
  ext p
  exact normalize_eq p

Похожие утверждения