Theorems · Theorem · commutative algebra

DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_lt

∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    ∀ {m k : ℕ},
      m + k < n →
        ∀ {x : A},
          x ∈ I →
            DividedPowers.OfInvertibleFactorial.dpow I m x * DividedPowers.OfInvertibleFactorial.dpow I k x =
              ↑((m + k).choose m) * DividedPowers.OfInvertibleFactorial.dpow I (m + k) x

Defined in: Mathlib.RingTheory.DividedPowers.RatAlgebra
Cited by: 1 results in Mathlib
Foundations: Depth 58 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.

Cites19

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
Idealstatement and proof · cited by 4,748
mul_commproof · cited by 2,262
mul_assocproof · cited by 1,667
IsUnitstatement and proof · cited by 1,602
Nat.factorialstatement and proof · cited by 616
Nat.choosestatement and proof · cited by 494
lt_of_le_of_ltproof · cited by 432
pow_addproof · cited by 315
Ring.inverseproof · cited by 160
le_self_addproof · cited by 68
le_add_selfproof · cited by 51

Cited by1

Results whose statement or proof uses this declaration.

DividedPowers.OfInvertibleFactorial.mul_dpowproof · cited by 0