chainBotCoeff_eq_zero — Mathlib

English

There exists a function f: ι → ℕ with support contained in b.support such that P.root i equals either the sum ∑ f j • P.root j or its negation; i.e., root i is a nonnegative integral combination of roots in the base, possibly negated.

Русский

Существует функция f: ι → ℕ, опорка которой содержится в b.support, такая что корень i равен либо сумме ∑ f j • P.root j, либо ее противоположности.

LaTeX

$$∃ f : ι → ℕ, f.support ⊆ b.support ∧ (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j)$$

Lean4

@[simp]
theorem chainBotCoeff_eq_zero : P.chainBotCoeff i j = 0 :=
  chainBotCoeff_eq_zero_iff.mpr <| Or.inr <| b.sub_notMem_range_root j.property i.property

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