esymmAlgHom_injective — Mathlib

English

For σ and R, if card σ ≤ n, then esymmAlgHom σ R n is injective.

Русский

Пусть σ и R заданы. Если кардинал σ не превосходит n, то esymmAlgHom σ R n инъективен.

LaTeX

$$$\operatorname{Injective} (\operatorname{esymmAlgHom} \sigma\, R\, n)$, при условии $n \le |\sigma|$$$

Lean4

theorem esymmAlgHom_injective (hn : n ≤ Fintype.card σ) : Function.Injective (esymmAlgHom σ R n) :=
  by
  rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]
  exact (AlgEquiv.injective _).comp (esymmAlgHom_fin_injective R hn)

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