pointwise_central_scalar

Mathlib.Algebra.Ring.Subring.Pointwise

URI: https://scilib.ai/kg/mathlib#Subring.pointwise_central_scalar

← MathLib Explorer

English

If M acts centrally on R, then M acts centrally on Subring R.

Русский

Если M действует центрально на R, то M действует центрально на Subring R.

LaTeX

$$$IsCentralScalar M (Subring R)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru