one — Mathlib

English

The symmetric subalgebra of MvPolynomial σ R is the subalgebra consisting of all symmetric polynomials.

Русский

Симметрическая подалгебра MvPolynomial σ R состоит из всех симметрических полиномов.

LaTeX

$$def symmetricSubalgebra (σ R : Type*) [CommSemiring R] : Subalgebra R (MvPolynomial σ R) := ...$$

Lean4

@[simp]
theorem one : IsSymmetric (1 : MvPolynomial σ R) :=
  (symmetricSubalgebra σ R).one_mem

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