pointwise_smul_toSubring

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.pointwise_smul_toSubring

English

The action by g on a subring corresponds to the action on its underlying substructure.

Русский

Действие g на подкольцо соответствует действию на его базовую подструктуру.

LaTeX

$$g•S.toSubring = (g•S).toSubring$$

Lean4

@[simp]
theorem pointwise_smul_toSubring (g : G) (S : ValuationSubring K) : (g • S).toSubring = g • S.toSubring :=
  rfl

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

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

Разделы

Аффилиация

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