symmetricSubalgebra — Mathlib

English

For an arbitrary φ in MvPolynomial σ R and an equivalence e: σ ≃ σ, φ is symmetric if and only if rename e φ is symmetric.

Русский

Для произвольного полинома φ в MvPolynomial σ R и биекция e: σ ≃ σ верно: φ симметричен тогда и только тогда, когда rename e φ симметричен.

LaTeX

$$(rename e φ).IsSymmetric ↔ φ.IsSymmetric$$

Lean4

/-- The subalgebra of symmetric `MvPolynomial`s. -/
def symmetricSubalgebra (σ R : Type*) [CommSemiring R] : Subalgebra R (MvPolynomial σ R)
    where
  carrier := setOf IsSymmetric
  algebraMap_mem' r e := rename_C e r
  mul_mem' ha hb e := by rw [map_mul, ha, hb]
  add_mem' ha hb e := by rw [map_add, ha, hb]

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