English
Given a MulSemiringAction G on R, there is a homomorphism toRingAut: G →* RingAut(R), sending g to the corresponding ring automorphism of R.
Русский
Если G действует на кольце R и действует через автоморфизмы, существует гомоморфизм toRingAut: G →* RingAut(R), отправляющий элемент g в соответствующий кольцевой автоморфизм R.
LaTeX
$$$[\\MulSemiringAction G R] \\Rightarrow G \\to^* \\operatorname{RingAut}(R)$ with $\\text{toFun}(g) = \\text{MulSemiringAction.toRingEquiv } G R\; g$$$
Lean4
/-- Each element of the group defines a ring automorphism.
This is a stronger version of `DistribMulAction.toAddAut` and
`MulDistribMulAction.toMulAut`. -/
@[simps]
def _root_.MulSemiringAction.toRingAut [MulSemiringAction G R] : G →* RingAut R
where
toFun := MulSemiringAction.toRingEquiv G R
map_mul' g h := RingEquiv.ext <| mul_smul g h
map_one' := RingEquiv.ext <| one_smul _
