apply_FaithfulSMul — Mathlib

English

The action of the permutation group on α is faithful: if f(a) = g(a) for all a ∈ α, then f = g.

Русский

Действие группы перестановок на α является верным: если f(a) = g(a) для всех a ∈ α, то f = g.

LaTeX

$$$ \forall f,g \in \mathrm{Perm}(\alpha), (\forall a \in \alpha, f(a) = g(a)) \Rightarrow f = g $$$

Lean4

/-- `Function.End.applyMulAction` is faithful. -/
instance apply_FaithfulSMul : FaithfulSMul (Function.End α) α where eq_of_smul_eq_smul := funext

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