count_span_normalizedFactors_eq_of_normUnit

English

If X is a unit in norm, the count of span X equals the count in the normalized factors after applying normalization.

Русский

Если X является нормализованной единицей, то число факторов спана X равно числу нормализованных факторов после нормализации.

LaTeX

$$Multiset.count (span{X}) (normalizedFactors(span{r})) = Multiset.count (normalize X) (normalizedFactors r)$$

Lean4

theorem count_span_normalizedFactors_eq_of_normUnit {r X : R} (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) :
    Multiset.count (Ideal.span { X } : Ideal R) (normalizedFactors (Ideal.span { r })) =
      Multiset.count X (normalizedFactors r) :=
  by simpa [hX₁, normalize_apply] using count_span_normalizedFactors_eq hr hX

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