esymmAlgHom_surjective — Mathlib

English

Let σ be finite and R a commutative ring. If card σ ≤ n, then esymmAlgHom σ R n is surjective.

Русский

Пусть σ — конечное множество и R — коммутативное кольцо. Если |σ| ≤ n, то esymmAlgHom σ R n сюръективно отображает.

LaTeX

$$$\operatorname{Surjective}(\operatorname{esymmAlgHom}(\sigma)\, R\, n)$, при $|\sigma| \le n$$$

Lean4

theorem esymmAlgHom_surjective (hn : Fintype.card σ ≤ n) : Function.Surjective (esymmAlgHom σ R n) :=
  by
  rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]
  exact (AlgEquiv.surjective _).comp (esymmAlgHom_fin_surjective R hn)

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