pairingIn_shortAddLong_left — Mathlib

English

The pair [shortRoot, longRoot] is linearly independent over R.

Русский

Пара [shortRoot, longRoot] линейно независима над R.

LaTeX

$$LinearIndependent_R([shortRoot(P), longRoot(P)])$$

Lean4

@[simp]
theorem pairingIn_shortAddLong_left :
    P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i :=
  by
  suffices P.pairing (shortAddLong P) i = P.pairing (short P) i + P.pairing (long P) i from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add]
  have : Fintype ι := Fintype.ofFinite ι
  have B := (P.posRootForm ℤ).toInvariantForm
  apply mul_right_cancel₀ (B.ne_zero i)
  rw [← B.two_mul_apply_root_root]
  simp [shortAddLongRoot_eq, mul_add, add_mul, B.two_mul_apply_root_root]

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