term_smulg

Mathlib.Tactic.Abel

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

Lean4

theorem term_smulg {α} [AddCommGroup α] (c n x a n' a') (h₁ : c * n = n') (h₂ : smulg c a = a') :
    smulg c (@termg α _ n x a) = termg n' x a' := by simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]

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

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

Разделы

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

Аффилиация

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