toAlgEquiv_injective — Mathlib

English

Each element of the group defines an algebra automorphism; hence G acts by algebra automorphisms via toAlgEquiv.

Русский

Каждый элемент группы задает алгебраический автоморфизм; поэтому G действует на алгебраические автоморфизмы через toAlgEquiv.

LaTeX

$$$ g \\mapsto \\mathrm{toAlgEquiv}_R(A)(g) \\in Aut_R(A). $$$

Lean4

theorem toAlgEquiv_injective [FaithfulSMul G A] :
    Function.Injective (MulSemiringAction.toAlgEquiv R A : G → A ≃ₐ[R] A) := fun _ _ h =>
  eq_of_smul_eq_smul fun r => AlgEquiv.ext_iff.1 h r

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