single_mul_apply_aux — Mathlib

English

Similarly, under suitable hypothesis H, (single m r * x) at m1 equals r · x(m2).

Русский

Аналогично, при подходящем условии H, (single m r * x) в m1 равно r · x(m2).

LaTeX

$$$\bigl( \operatorname{single}(m,r) * x \bigr)_{m_1} = r \cdot x(m_2)$ под условием $H$$$

Lean4

@[to_additive (dont_translate := R) single_mul_apply_aux]
theorem single_mul_apply_aux (H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂) : (single m r * x) m₁ = r * x m₂ := by
  classical
    calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]

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