English
If k is such that P.root k equals the sum P.root j plus P.root i, then the bottom coefficient at i,k equals the bottom coefficient at i,j plus one.
Русский
Если существует k с P.root k = P.root j + P.root i, то P.chainBotCoeff(i,k) = P.chainBotCoeff(i,j) + 1.
LaTeX
$$$$ P.chainBotCoeff(i, k) = P.chainBotCoeff(i, j) + 1 \quad\text{whenever}\quad P.root(k) = P.root(j) + P.root(i). $$$$
Lean4
theorem chainBotCoeff_of_add {k : ι} (hk : P.root k = P.root j + P.root i) :
P.chainBotCoeff i k = P.chainBotCoeff i j + 1 :=
by
have h' : LinearIndependent R ![P.root i, P.root k] := by simpa [hk, add_comm]
apply Nat.cast_injective (R := ℤ)
rw [Nat.cast_add, Nat.cast_one, coe_chainBotCoeff_eq_sSup h', coe_chainBotCoeff_eq_sSup h]
have (z : ℤ) : P.root k - z • P.root i = P.root j - (z - 1) • P.root i := by rw [hk]; module
replace this :
{z : ℤ | P.root k - z • P.root i ∈ range P.root} =
OrderIso.addRight 1 '' {n | P.root j - n • P.root i ∈ range P.root} :=
by simp [this, sub_eq_add_neg]
have bdd : BddAbove {z : ℤ | P.root j - z • P.root i ∈ range P.root} :=
by
rw [setOf_root_sub_zsmul_mem_eq_Icc h]
exact bddAbove_Icc
rw [this, ← OrderIso.map_csSup' _ ⟨0, by simp⟩ bdd, OrderIso.addRight_apply]
