mulDysonETransform_idem — Mathlib

English

Applying the Dyson e-transform twice with the same parameter e yields the same result as applying it once: mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x.

Русский

Повторное применение преобразования Дайсона с тем же параметром e дает тот же результат, что и первое применение: ...

LaTeX

$$mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x$$

Lean4

@[to_additive (attr := simp)]
theorem mulDysonETransform_idem : mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x :=
  by
  ext : 1 <;> dsimp
  · rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]
    exact inter_subset_union
  · rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
    exact inter_subset_union

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