Theorems · Theorem · general algebraic systems
Pi.single_eq_of_ne
∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] {i i' : ι},
i' ≠ i → ∀ (x : M i), Pi.single i x i' = 0- Defined in
- Mathlib.Algebra.Notation.Pi.Basic
- Cited by
- 116 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 21 definitions · uses no axioms
- Assumes
- ZeroDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Pi.singlestatement · cited by 518
- Function.update_of_neproof · cited by 198
Cited by116
Results whose statement or proof uses this declaration.
- Finsupp.single_eq_of_neproof · cited by 61
- Pi.single_eq_of_ne'proof · cited by 33
- Finset.affineCombination_piSingleproof · cited by 19
- single_dotProductproof · cited by 10
- HahnSeries.coeff_single_of_neproof · cited by 9
- Fintype.sum_single_smulproof · cited by 8
- MvPolynomial.pderiv_X_of_neproof · cited by 8
- Finset.affineCombinationLineMapWeights_apply_rightproof · cited by 5
- Matrix.adjugate_transposeproof · cited by 5
- ProbabilityTheory.setBernoulli_ae_subsetproof · cited by 5
- Affine.Simplex.point_mem_closedInteriorproof · cited by 5
- RootPairing.Base.height_one_of_mem_supportproof · cited by 4