hsymm_one — Mathlib

English

The 1st complete homogeneous symmetric polynomial equals the sum of the variables: hsymm(1) = ∑ i X_i.

Русский

Первый полный однородный симметрический полином равен сумме переменных: hsymm(1) = ∑ i X_i.

LaTeX

$$$ hsymm(\\sigma,R,1) = \\sum i, X_i $$$

Lean4

@[simp]
theorem hsymm_one : hsymm σ R 1 = ∑ i, X i := by
  symm
  apply Fintype.sum_equiv oneEquiv
  simp only [oneEquiv_apply, Multiset.map_singleton, Multiset.prod_singleton, implies_true]

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