pointwise_smul_toSubsemiring — Mathlib

English

The scalar action on Subalgebra translates to scalar action on Subsemiring: (m • S).toSubsemiring = m • S.toSubsemiring.

Русский

Скалярное действие на подалгебре переходит к скалярному действию на подполосе: (m • S).toSubsemiring = m • S.toSubsemiring.

LaTeX

$$ (m • S).toSubsemiring = m • S.toSubsemiring $$

Lean4

@[simp]
theorem pointwise_smul_toSubsemiring (m : R') (S : Subalgebra R A) : (m • S).toSubsemiring = m • S.toSubsemiring :=
  rfl

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