exp_sum_of_commute — Mathlib

English

For a finite family of commuting matrices indexed by ι, exp(sum f_i) equals the product over i of exp(f_i).

Русский

Для конечного множества попарно совместно коммутирующихся матриц {f_i} индексируемых i ∈ ι экспонента суммы равна произведению экспонент отдельных членов: exp(∑ f_i) = ∏ exp(f_i).

LaTeX

$$$\\exp\\_\\mathbb{K}\\Big(\\sum_{i \\in s} f_i\\Big) = \\prod_{i \\in s}^{\\text{noncomm}} \\exp\\_\\mathbb{K}(f_i)$, при условии совместного коммутирования$$

Lean4

nonrec theorem exp_sum_of_commute {ι} (s : Finset ι) (f : ι → Matrix m m 𝔸) (h : (s : Set ι).Pairwise (Commute on f)) :
    exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) fun _ hi _ hj _ => (h.of_refl hi hj).exp 𝕂 :=
  open scoped Norms.Operator in exp_sum_of_commute s f h

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