pow_subst

Mathlib.Tactic.CancelDenoms.Core

URI: https://scilib.ai/kg/mathlib#CancelDenoms.pow_subst

Lean4

theorem pow_subst {α} [CommRing α] {n e1 t1 k l : α} {e2 : ℕ} (h1 : n * e1 = t1) (h2 : l * n ^ e2 = k) :
    k * (e1 ^ e2) = l * t1 ^ e2 := by rw [← h2, ← h1, mul_pow, mul_assoc]

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

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

Разделы

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

Аффилиация

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