toRingEquiv — Mathlib

English

There is a canonical mapping from a group action to a ring automorphism group; the action by each group element corresponds to a ring automorphism of R, forming a homomorphism into RingAut(R).

Русский

Существует каноническое отображение из группы действующих на R в группу кольцевых автоморфизмов RingAut(R); действие каждого элемента порождает кольцевой автоморфизм, образующий гомоморфизм в RingAut(R).

LaTeX

$$$G \\to^* RingAut(R)$, $g \\mapsto (r \\mapsto g \\cdot r)$$$

Lean4

/-- Each element of the group defines a semiring isomorphism. -/
@[simps!]
def toRingEquiv [MulSemiringAction G R] (x : G) : R ≃+* R :=
  { DistribMulAction.toAddEquiv R x, MulSemiringAction.toRingHom G R x with }

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