isSymmetric_rename — Mathlib

English

For any φ and equivalence e, (rename e φ).IsSymmetric ↔ φ.IsSymmetric.

Русский

Для любого φ и эквивалентности e выполняется: (rename e φ) симметричен тогда и только тогда, когда φ симметричен.

LaTeX

$$MvPolynomial.IsSymmetric.rename φ e$$

Lean4

@[simp]
theorem _root_.MvPolynomial.isSymmetric_rename {e : σ ≃ τ} : (MvPolynomial.rename e φ).IsSymmetric ↔ φ.IsSymmetric :=
  ⟨fun h => by simpa using (IsSymmetric.rename (R := R) h e.symm), (IsSymmetric.rename · e)⟩

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