Theorems · Theorem · order theory
DFinsupp.tsub_apply
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
[inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
[inst_4 : ∀ (i : ι), OrderedSub (α i)] (f g : Π₀ (i : ι), α i) (i : ι), (f - g) i = f i - g i- Defined in
- Mathlib.Data.DFinsupp.Order
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- DFinsuppstatement and proof · cited by 694
- OrderedSubstatement and proof · cited by 236
- CanonicallyOrderedAddstatement and proof · cited by 229
- DFinsupp.zipWith_applyproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- DFinsupp.coe_tsubproof · cited by 2
- DFinsupp.single_tsubproof · cited by 0