smul_mk'_self

Mathlib.RingTheory.Localization.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalization.smul_mk'_self

English

For m ∈ M and r ∈ R, m • mk' S r m equals the algebra map of r in S.

Русский

Для m ∈ M и r ∈ R, m • mk' S r m = algebraMap_R^S(r).

LaTeX

$$$m \\cdot mk' S r m = (algebraMap R S) r$$$

Lean4

@[simp]
theorem smul_mk'_self {m : M} {r : R} : (m : R) • mk' S r m = algebraMap R S r := by rw [smul_mk', mk'_mul_cancel_left]

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

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

Разделы

Аффилиация

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