isMinimal — Mathlib

English

There exists a minimal solution in the Solution structure for the three-gen framework.

Русский

Существует минимальное решение в структуре Solution трёхгенераторной схемы.

LaTeX

$$$\exists S_1: \text{Solution } h\zeta, S_1\text{ isMinimal}$$$

Lean4

/-- We say that `S : Solution` is minimal if for all `S₁ : Solution`, the multiplicity of `λ` in
`S.c` is less or equal than the multiplicity in `S₁.c`. -/
def isMinimal : Prop :=
  ∀ (S₁ : Solution hζ), S.multiplicity ≤ S₁.multiplicity

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