fst_pow — Mathlib

English

For any x in GradedMonoid A and any natural number n, the first component of x^n equals n times the first component of x.

Русский

Для любого элемента x в GradedMonoid A и любого натурального числа n первая компонента x^n равна n-кратной первой компоненте x.

LaTeX

$$$\\mathrm{fst}(x^n) = n \\cdot \\mathrm{fst}(x)$$$

Lean4

@[simp]
theorem fst_pow [AddMonoid ι] [GMonoid A] (x : GradedMonoid A) (n : ℕ) : (x ^ n).fst = n • x.fst :=
  rfl

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