Solution'_descent_multiplicity — Mathlib

English

The descended multiplicity equals S.multiplicity - 1.

Русский

Кратность нисходящей последовательности равна S.multiplicity - 1.

LaTeX

$$Solution'_descent_multiplicity : S.Solution'_descent.multiplicity = S.multiplicity - 1$$

Lean4

/-- We have that `S.Solution'_descent.multiplicity = S.multiplicity - 1`. -/
theorem Solution'_descent_multiplicity : S.Solution'_descent.multiplicity = S.multiplicity - 1 :=
  by
  refine multiplicity_eq_of_dvd_of_not_dvd (by simp [Solution'_descent]) (fun h ↦ S.lambda_not_dvd_X ?_)
  obtain ⟨k, hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k⟩ := h
  rw [pow_succ, mul_assoc] at hk
  simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq, false_and, or_false] at hk
  simp [hk]

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