Theorems · Theorem · general algebraic systems
Finsupp.unique_ext
∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Unique α] {f g : α →₀ M}, f default = g default → f = g- Defined in
- Mathlib.Data.Finsupp.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Uniquestatement and proof · cited by 400
- Finsupp.extproof · cited by 399
- Unique.eq_defaultproof · cited by 38
Cited by11
Results whose statement or proof uses this declaration.
- PowerSeries.WithPiTopology.tendsto_iff_coeff_tendstoproof · cited by 5
- rank_eq_zero_iffproof · cited by 3
- MvPolynomial.toMvPowerSeries_pUnitAlgEquivproof · cited by 3
- PowerSeries.hasSum_eval₂proof · cited by 2
- PowerSeries.hasSum_of_monomials_selfproof · cited by 2
- MvPolynomial.C_surjectiveproof · cited by 2
- Finsupp.unique_ext_iffproof · cited by 1
- Module.Basis.basis_singleton_iffproof · cited by 1
- AddEquiv.finsuppUnique_symmproof · cited by 0
- PowerSeries.le_weightedOrder_substproof · cited by 0
- Finsupp.LinearEquiv.finsuppUnique_symm_applyproof · cited by 0