Theorems · Definition · group theory
AddMonoidHom.mker
{M : Type u_1} →
{N : Type u_2} →
[inst : AddZeroClass M] →
[inst_1 : AddZeroClass N] →
{F : Type u_4} → [inst_2 : FunLike F M N] → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid MThe additive kernel of an AddMonoidHom is the AddSubmonoid of elements such that
f x = 0.
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botproof · cited by 4,720
- FunLikestatement and proof · cited by 2,560
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement · cited by 1,178
- AddMonoidHomClassstatement and proof · cited by 252
- AddSubmonoid.comapproof · cited by 62
Cited by20
Results whose statement or proof uses this declaration.
- AddMonoidHom.kerproof · cited by 158
- AddMonoidHom.mem_mkerstatement · cited by 4
- DFinsupp.mker_mapRangeAddMonoidHomstatement and proof · cited by 3
- AddMonoidHom.domRestrict_mkerstatement · cited by 1
- AddMonoidHom.comap_bot'statement · cited by 1
- AddMonoidHom.mker_inlstatement · cited by 1
- AddMonoidHom.mker_inrstatement · cited by 1
- AddMonoidHom.restrict_mkerstatement · cited by 0
- AddMonoidHom.comap_mkerstatement · cited by 0
- AddMonoidHom.ker_toAddSubmonoidstatement · cited by 0
- AddMonoidHom.mker.congr_simpstatement and proof · cited by 0
- AddMonoid.Coprod.mker_swapstatement · cited by 0