English
If a is irreducible and b ≠ 0, then emultiplicity a b equals the count of normalize a in normalizedFactors b.
Русский
Если a неразложимо и b ≠ 0, то кратность emultiplicity a b равна количеству встречаемостей normalize a в normalizedFactors b.
LaTeX
$$$emultiplicity\ a\ b = (normalizedFactors\ b).count(\normalize a)$$$
Lean4
/-- The multiplicity of an irreducible factor of a nonzero element is exactly the number of times
the normalized factor occurs in the `normalizedFactors`.
See also `count_normalizedFactors_eq` which expands the definition of `multiplicity`
to produce a specification for `count (normalizedFactors _) _`..
-/
theorem emultiplicity_eq_count_normalizedFactors [DecidableEq R] {a b : R} (ha : Irreducible a) (hb : b ≠ 0) :
emultiplicity a b = (normalizedFactors b).count (normalize a) :=
by
apply le_antisymm
· apply Order.le_of_lt_add_one
rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge, le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ←
le_count_iff_replicate_le]
simp
rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
