Theorems · Theorem · general algebraic systems
Finsupp.ext
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f g : α →₀ M}, (∀ (a : α), f a = g a) → f = g- Defined in
- Mathlib.Data.Finsupp.Defs
- Cited by
- 399 results in Mathlib
- Foundations
- Depth 59 from the axioms, rests on 816 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- DFunLike.extproof · cited by 240
Cited by399
Results whose statement or proof uses this declaration.
- MvPolynomial.extproof · cited by 61
- Nat.factorization_zeroproof · cited by 32
- Module.Free.of_equivproof · cited by 23
- AddMonoidAlgebra.mapDomain_singleproof · cited by 23
- Finsupp.mapDomain_injectiveproof · cited by 16
- Nat.factorization_mulproof · cited by 14
- Finsupp.embDomain_eq_mapDomainproof · cited by 13
- Polynomial.X_mulproof · cited by 12
- MonoidAlgebra.mapDomain_singleproof · cited by 12
- Finsupp.unique_extproof · cited by 11
- Finsupp.equivMapDomain_singleproof · cited by 11
- Finsupp.lcongr_symmproof · cited by 11
Showing the 200 most cited of 399.