Theorems · Theorem · general algebraic systems
Finsupp.single_eq_of_ne
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M}, a' ≠ a → (fun₀ | a => b) a' = 0- Defined in
- Mathlib.Data.Finsupp.Single
- Cited by
- 61 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Finsuppstatement · cited by 5,255
- Finsupp.singlestatement · cited by 943
- Pi.single_eq_of_neproof · cited by 116
Cited by61
Results whose statement or proof uses this declaration.
- Matrix.toLin_selfproof · cited by 9
- Ordinal.CNF.eval_single_add'proof · cited by 5
- Complex.coe_basisOneIproof · cited by 5
- Finsupp.some_single_noneproof · cited by 5
- Finsupp.update_eq_erase_add_singleproof · cited by 4
- IsBaseChange.basis_repr_comp_applyproof · cited by 3
- Finsupp.sumElim_zero_singleproof · cited by 3
- Polynomial.homogenize_X_powproof · cited by 3
- Finsupp.eq_single_iffproof · cited by 3
- exteriorPower.ιMultiDual_apply_nondiagproof · cited by 3
- Finsupp.Lex.single_strictAntiproof · cited by 3
- Finsupp.update_eq_single_add_eraseproof · cited by 2