mk'_eq_mk'_iff

Mathlib.Algebra.Module.LocalizedModule.Basic

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

← MathLib Explorer

English

mk' f m s = 0 iff f m = 0 when s ∈ S.

Русский

mk' f m s = 0 тогда и только тогда, когда f m = 0.

LaTeX

$$$mk' f m s = 0 \\iff f m = 0$$$

Lean4

theorem mk'_eq_mk'_iff (m₁ m₂ : M) (s₁ s₂ : S) : mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ s : S, s • s₁ • m₂ = s • s₂ • m₁ :=
  by
  delta mk'
  rw [(fromLocalizedModule.inj S f).eq_iff, LocalizedModule.mk_eq]
  simp_rw [eq_comm]

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

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

Разделы

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

Аффилиация

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