diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean
index 6ba6a3b5905e95..13eab4c707a4fd 100644
--- a/Mathlib/Data/Nat/Choose/Sum.lean
+++ b/Mathlib/Data/Nat/Choose/Sum.lean
@@ -235,4 +235,11 @@ theorem sum_antidiagonal_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
   simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n
 #align finset.sum_antidiagonal_choose_succ_mul Finset.sum_antidiagonal_choose_succ_mul
 
+theorem sum_antidiagonal_choose_add (d n : ℕ) :
+    (Finset.sum (antidiagonal n) fun ij => (d + ij.2).choose d) =
+    (d + n).choose d + (d + n).choose (succ d) := by
+  induction n with
+  | zero => simp
+  | succ n hn => simpa [Nat.sum_antidiagonal_succ] using hn
+
 end Finset
diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean
index 2fc1d7cbe3b573..872db3c808f832 100644
--- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean
+++ b/Mathlib/RingTheory/PowerSeries/WellKnown.lean
@@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import Mathlib.RingTheory.PowerSeries.Basic
 import Mathlib.Data.Nat.Parity
+import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
 
 #align_import ring_theory.power_series.well_known from "leanprover-community/mathlib"@"8199f6717c150a7fe91c4534175f4cf99725978f"
@@ -66,6 +67,79 @@ theorem map_invUnitsSub (f : R →+* S) (u : Rˣ) :
 
 end Ring
 
+section invOneSubPow
+
+variable {S : Type*} [CommRing S] (d : ℕ)
+
+/--
+(1 + X + X^2 + ...) * (1 - X) = 1.
+
+Note that the power series `1 + X + X^2 + ...` is written as `mk 1` where `1` is the constant
+function so that `mk 1` is the power series with all coefficients equal to one.
+-/
+theorem mk_one_mul_one_sub_eq_one : (mk 1 : S⟦X⟧) * (1 - X) = 1 := by
+  rw [mul_comm, ext_iff]
+  intro n
+  by_cases hn : n = 0
+  · subst hn
+    simp only [coeff_zero_eq_constantCoeff, map_mul, map_sub, map_one, constantCoeff_X, sub_zero,
+      one_mul, coeff_one, ↓reduceIte]
+    rfl
+  · rw [show n = n - 1 + 1 by exact (Nat.succ_pred hn).symm, sub_mul]
+    simp
+
+/--
+Note that `mk 1` is the constant function `1` so the power series `1 + X + X^2 + ...`. This theorem
+states that for any `d : ℕ`, `(1 + X + X^2 + ... : S⟦X⟧) ^ (d + 1)` is equal to the power series
+`mk fun n => Nat.choose (d + n) d : S⟦X⟧`.
+-/
+theorem mk_one_pow_eq_mk_choose_add :
+    (mk 1 : S⟦X⟧) ^ (d + 1) = (mk fun n => Nat.choose (d + n) d : S⟦X⟧) := by
+  induction d with
+  | zero => ext; simp
+  | succ d hd =>
+      ext n; rw [Nat.succ_eq_add_one, pow_add, hd, pow_one, mul_comm, coeff_mul]
+      simp_rw [coeff_mk, Pi.one_apply, one_mul]; norm_cast
+      rw [Finset.sum_antidiagonal_choose_add, ← Nat.choose_succ_succ]; congr
+      exact add_right_comm d n 1
+
+/--
+The power series `mk fun n => Nat.choose (d + n) d`, whose multiplicative inverse is
+`(1 - X) ^ (d + 1)`.
+-/
+noncomputable def invOneSubPow : S⟦X⟧ˣ where
+  val := mk fun n => Nat.choose (d + n) d
+  inv := (1 - X) ^ (d + 1)
+  val_inv := by
+    rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
+  inv_val := by
+    rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
+
+theorem invOneSubPow_val_eq_mk_choose_add :
+    (invOneSubPow d).val = (mk fun n => Nat.choose (d + n) d : S⟦X⟧) := rfl
+
+theorem invOneSubPow_val_zero_eq_invUnitSub_one :
+    (invOneSubPow 0).val = invUnitsSub (1 : Sˣ) := by
+  simp [invOneSubPow, invUnitsSub]
+
+/--
+The theorem `PowerSeries.mk_one_mul_one_sub_eq_one` implies that `1 - X` is a unit in `S⟦X⟧`
+whose inverse is the power series `1 + X + X^2 + ...`. This theorem states that for any `d : ℕ`,
+`PowerSeries.invOneSubPow d` is equal to `(1 - X)⁻¹ ^ (d + 1)`.
+-/
+theorem invOneSubPow_eq_inv_one_sub_pow :
+    invOneSubPow d = (Units.mkOfMulEqOne (1 - X) (mk 1 : S⟦X⟧)
+    <| Eq.trans (mul_comm _ _) mk_one_mul_one_sub_eq_one)⁻¹ ^ (d + 1) := by
+  rw [inv_pow]
+  exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow d) <| by
+    rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
+    exact (invOneSubPow d).inv_val).symm
+
+theorem invOneSubPow_inv_eq_one_sub_pow :
+    (invOneSubPow d).inv = (1 - X : S⟦X⟧) ^ (d + 1) := rfl
+
+end invOneSubPow
+
 section Field
 
 variable (A A' : Type*) [Ring A] [Ring A'] [Algebra ℚ A] [Algebra ℚ A']