mk_smul

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.torsionBySet.mk_smul

English

In the torsionBySet submodule, the induced smul by the quotient equals the original smul: [I] b • x = b • x.

Русский

В подмодуле torsionBySet скалярное умножение по содержимому произведения совпадает: [b]_I • x = b • x.

LaTeX

$$Ideal.Quotient.mk I b • x = b • x$$

Lean4

@[simp]
theorem mk_smul (I : Ideal R) (b : R) (x : torsionBySet R M I) : Ideal.Quotient.mk I b • x = b • x :=
  rfl

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

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

Разделы

Аффилиация

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