Theorems · Theorem · commutative algebra

PowerSeries.coeff_log

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (n : ℕ),
  (PowerSeries.coeff n) (PowerSeries.log A) = if n = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1) / ↑n)

Defined in

Mathlib.RingTheory.PowerSeries.Log

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAlgebra