∀ (σ : Type u_2) (R : Type u_1) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R],
  Fintype.card σ = n →
    Function.Injective ⇑(MvPolynomial.esymmAlgHom σ R n) ∧ Function.Surjective ⇑(MvPolynomial.esymmAlgHom σ R n)