Theorems · Theorem · commutative algebra

DividedPowers.OfInvertibleFactorial.dpow_add

∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    I ^ n = 0 →
      ∀ {m : ℕ} {x : A},
        x ∈ I →
          ∀ {y : A},
            y ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (x + y) =
                ∑ k ∈ Finset.HasAntidiagonal.antidiagonal m,
                  DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y

Defined in: Mathlib.RingTheory.DividedPowers.RatAlgebra
Cited by: 0 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring DecidablePred

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommSemiringstatement and proof · cited by 10,911
SetLike.coeproof · cited by 8,199
Finset.sumstatement and proof · cited by 5,195
Idealstatement and proof · cited by 4,748
mul_commproof · cited by 2,262
MulZeroClass.mul_zeroproof · cited by 2,091
mul_assocproof · cited by 1,667
IsUnitstatement and proof · cited by 1,602
add_commproof · cited by 1,535
Nat.factorialstatement and proof · cited by 616
pow_addproof · cited by 315
Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218

Cited by1

Results whose statement or proof uses this declaration.

DividedPowers.OfInvertibleFactorial.dividedPowersproof · cited by 2