pointwise_central_scalar — Mathlib

English

For any a, a•S equals the comap of S under the appropriate ring automorphism, i.e., a•S = S.comap (MulSemiringAction.toRingAut a).symm.

Русский

Для любого a: a•S равняется обратному образу S через соответствующий кольцевой автоморфизм, то есть a•S = S.comap (MulSemiringAction.toRingAut a).symm.

LaTeX

$$$a\cdot S = S^{\mathrm{comap}}(toRingAut(a))$$$

Lean4

instance pointwise_central_scalar [MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R] : IsCentralScalar M (Ideal R) :=
  ⟨fun _ S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩

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