mk'_cancel_left

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalizedModule.mk'_cancel_left

← MathLib Explorer

English

If f is multiplicative on M, then mk' f m1 s1 · mk' f m2 s2 = mk' f (m1 m2) (s1 s2).

Русский

Если f сохраняет умножение, то mk' f m1 s1 · mk' f m2 s2 = mk' f (m1 m2) (s1 s2).

LaTeX

$$$mk' f m_1 s_1 \\cdot mk' f m_2 s_2 = mk' f (m_1 m_2) (s_1 s_2)$$$

Lean4

@[simp]
theorem mk'_cancel_left (m : M) (s₁ s₂ : S) : mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂ :=
  by
  delta mk'
  rw [LocalizedModule.mk_cancel_common_left]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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