term_smul

Mathlib.Tactic.Abel

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Abel.term_smul

Lean4

theorem term_smul {α} [AddCommMonoid α] (c n x a n' a') (h₁ : c * n = n') (h₂ : smul c a = a') :
    smul c (@term α _ n x a) = term n' x a' := by simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']

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

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

Разделы

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

Аффилиация

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