Theorems · Theorem · commutative algebra

PowerSeries.map_exp

∀ {A : Type u_1} {A' : Type u_2} [inst : Ring A] [inst_1 : Ring A'] [inst_2 : Algebra ℚ A] [inst_3 : Algebra ℚ A']
  (f : A →+* A'), (PowerSeries.map f) (PowerSeries.exp A) = PowerSeries.exp A'

Defined in

Mathlib.RingTheory.PowerSeries.Exp

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingAlgebraAlgebra