leOnePart_apply — Mathlib

English

In a family of groups indexed by i, the negative part applied pointwise yields (f⁻ᵐ)(i) = (f(i))⁻ᵐ.

Русский

В семействе групп, индексируемом по i, отрицательная часть применяется по каждому индексу: (f⁻ᵐ)(i) = (f(i))⁻ᵐ.

LaTeX

$$f^{-m}(i) = (f(i))^{-m}$$

Lean4

@[to_additive (attr := simp)]
theorem leOnePart_apply (f : ∀ i, α i) (i : ι) : f⁻ᵐ i = (f i)⁻ᵐ :=
  rfl

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