Commit 2026-04-08 19:05 11027af8

View on Github →

feat(RingTheory/PowerSeries): Construction of Q such that P(Q(X)) = X (#26645) This contribution was created as part of the ZMC conference 2025 "Anabelian Geometry and its Computer Formalization".

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.coeff_one_substInv

added theorem PowerSeries.coeff_subst_sum_C_substInvFun_mul_X_pow_sub_X

added theorem PowerSeries.constantCoeff_substInv

added theorem PowerSeries.hasSubst_substInv

added def PowerSeries.substInv

added def PowerSeries.substInvFun

added theorem PowerSeries.subst_substInv_left

added theorem PowerSeries.subst_substInv_right