Theorems · Definition · group theory
AddMonoidHom.single
{I : Type u} →
(f : I → Type v) → [DecidableEq I] → [inst : (i : I) → AddZeroClass (f i)] → (i : I) → f i →+ (i : I) → f iThe additive monoid homomorphism including a single additive monoid into a dependent family
of additive monoids, as functions supported at a point.
This is the AddMonoidHom version of Pi.single.
- Defined in
- Mathlib.Algebra.Group.Pi.Lemmas
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqAddZeroClass
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.
- AddMonoidHomstatement · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
- ZeroHomproof · cited by 161
- ZeroHom.singleproof · cited by 2
Cited by22
Results whose statement or proof uses this declaration.
- LinearMap.singleproof · cited by 62
- Pi.single_addproof · cited by 4
- Pi.single_negproof · cited by 3
- Pi.single_subproof · cited by 3
- AddSubgroup.pi_le_iffstatement · cited by 2
- AddSubmonoid.pi_le_iffstatement and proof · cited by 2
- Finset.noncommSum_singleproof · cited by 2
- AddMonoidHom.functions_ext'statement and proof · cited by 1
- AddSubmonoid.iSup_map_singlestatement and proof · cited by 1
- AddSubmonoid.iSup_map_single_lestatement · cited by 1
- Pi.single_nsmulproof · cited by 1
- AddSubgroup.addCommutator_pi_pi_of_finiteproof · cited by 1