coe_pointwise_smul

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

If x ∈ S, then g•x ∈ g•S for any g ∈ G.

Русский

Если x ∈ S, то для любого g ∈ G верно g•x ∈ g•S.

LaTeX

$$x ∈ S ⇒ g•x ∈ g•S$$

Lean4

@[simp]
theorem coe_pointwise_smul (g : G) (S : ValuationSubring K) : ↑(g • S) = g • (S : Set K) :=
  rfl

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

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

Разделы

Аффилиация

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