mulShift_spec'

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.mulShift_spec'

← MathLib Explorer

English

If n is a natural number, then mulShift ψ n x = ψ(x)^n.

Русский

Если n натуральное, то mulShift ψ n x = ψ(x)^n.

LaTeX

$$$$\operatorname{mulShift}(\psi, n, x) = \psi(x)^n.$$$$

Lean4

/-- If `n` is a natural number, then `mulShift ψ n x = (ψ x) ^ n`. -/
theorem mulShift_spec' (ψ : AddChar R M) (n : ℕ) (x : R) : mulShift ψ n x = ψ x ^ n := by
  rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]

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

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

Разделы

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

Аффилиация

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