English
For a given Solution, there is a well-defined notion of multiplicity of λ in its c, which is an integer measure of how many times λ divides c.
Русский
У решения существует понятие кратности λ в элементе c, которая измеряется целым числом.
LaTeX
$$$\text{multiplicity}:=\#\{\text{times } \lambda \text{ divides } c\}$$$
Lean4
@[macro _private.Mathlib.NumberTheory.FLT.Three.0.«termλ»]
public meta def «_aux_Mathlib_NumberTheory_FLT_Three___macroRules__private_Mathlib_NumberTheory_FLT_Three_0_termλ_1» :
Macro✝ := fun
| `(λ) => `(hζ.toInteger - 1)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
