chainBotCoeff — Mathlib

English

As in 133551, the map i ↦ P.pairingIn ℤ i k is injective for fixed k.

Русский

Как и ранее, отображение i ↦ P.pairingIn ℤ i k инъективно по i при фиксированном k.

LaTeX

$$Injective (fun i ↦ P.pairingIn ℤ i k)$$

Lean4

/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the value `q ≥ 0` where
`β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.

In the absence of linear independence, it takes a junk value. -/
def chainBotCoeff : ℕ :=
  if h : LinearIndependent R ![P.root i, P.root j] then
    (-(P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose).toNat
  else 0

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