multiplicity_lambda_c_finite — Mathlib

English

Summarizes the polynomial versions of Fermat's Last Theorem across abc-type results with coprimeness assumptions.

Русский

Сумма всех полиномных версий Ферматовой теоремы для abc-подобных случаев при взаимной простоте.

LaTeX

$$$\text{Polynomial FLT} \Rightarrow (\text{abc-type bounds} \lor \text{derivatives vanish})$$$

Lean4

/-- For any `S' : Solution'`, the multiplicity of `λ` in `S'.c` is finite. -/
theorem multiplicity_lambda_c_finite : FiniteMultiplicity (hζ.toInteger - 1) S'.c :=
  .of_not_isUnit hζ.zeta_sub_one_prime'.not_unit S'.hc

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