Theorem: PowerSeries.isExponential_neg_mul_self_eq_one (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ scale (-1) f * f = 1
Tactic:
rw [mul_comm, isExponential_self_mul_neg_eq_one hf]
State after:
no goals