English
For a nonzero, nonunit p in a CancelCommMonoidWithZero α, the p-multiplicity of p^n equals n for all n.
Русский
Для не нулевого и не единицы p в CancelCommMonoidWithZero α кратность p относительно p^n равна n.
LaTeX
$$$ \forall {n : \mathbb{N}}, multiplicity p (p^n) = n$$$
Lean4
@[simp]
theorem multiplicity_self {a : α} : multiplicity a a = 1 :=
by
by_cases ha : FiniteMultiplicity a a
· rw [ha.multiplicity_eq_iff]
simp only [pow_one, dvd_refl, reduceAdd, true_and]
rintro ⟨v, hv⟩
nth_rw 1 [← mul_one a] at hv
simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv
obtain hv | rfl := hv
· have : IsUnit a := isUnit_of_mul_eq_one a v hv.symm
simpa [this] using ha.not_unit
· simpa using ha.ne_zero
· simp [ha]
