smul_eq_eval

Mathlib.Tactic.Module

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Module.NF.smul_eq_eval

Lean4

theorem smul_eq_eval {R₀ : Type*} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₀] [Module R₀ M] [Semiring S]
    [Module S M] {l : NF R M} {l₀ : NF R₀ M} {s : S} {r : R} {x : M} (hx : x = l₀.eval) (hl : l.eval = l₀.eval)
    (hs : r • x = s • x) : s • x = (r • l).eval :=
  by
  rw [← hs, hx, ← hl, eval_smul]
  rfl

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

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

Разделы

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

Аффилиация

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