Theorem Commute.exp_right

Modification history

2023-11-17 14:37

Mathlib/Analysis/NormedSpace/Exponential.lean

chore: exp -> NormedSpace.exp (#8436) …

Modified Commute.exp_right View on Github →

2023-06-02 10:22

Mathlib/Analysis/NormedSpace/Exponential.lean

feat: port Analysis.NormedSpace.Exponential (#4567)

Added Commute.exp_right View on Github →