Commit 2022-05-02 20:22 17412076

View on Github →

feat(analysis/normed_space/exponential): Aeᴮ = eᴮA if AB = BA (#13881) This commit shows that the exponenential commutes if the exponent does. This generalizes a previous weaker result.

Estimated changes

Modified src/analysis/normed_space/exponential.lean

modified theorem commute.exp

added theorem commute.exp_left

added theorem commute.exp_right

Modified src/topology/algebra/infinite_sum.lean

added theorem commute.tsum_left

added theorem commute.tsum_right