Theorems · Definition · functional analysis
NormedAddGroupHom.ker
{V₁ : Type u_3} →
{V₂ : Type u_4} →
[inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → AddSubgroup V₁The kernel of a bounded group homomorphism. Naturally endowed with a
SeminormedAddCommGroup instance.
- Defined in
- Mathlib.Analysis.Normed.Group.Hom
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 101 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.
- AddSubgroupstatement · cited by 3,232
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- NormedAddGroupHomstatement and proof · cited by 216
- AddMonoidHom.kerproof · cited by 158
- NormedAddGroupHom.toAddMonoidHomproof · cited by 13
Cited by19
Results whose statement or proof uses this declaration.
- NormedAddGroupHom.equalizerproof · cited by 14
- NormedAddGroupHom.ker.liftstatement · cited by 3
- NormedAddGroupHom.mem_kerstatement · cited by 2
- NormedAddGroupHom.IsQuotient.normstatement · cited by 2
- AddSubgroup.ker_normedMkstatement · cited by 2
- NormedAddGroupHom.isClosed_kerstatement · cited by 1
- NormedAddGroupHom.ker_le_ker_completionstatement and proof · cited by 1
- NormedAddGroupHom.coe_kerstatement · cited by 1
- NormedAddGroupHom.IsQuotient.norm_leproof · cited by 1
- SemiNormedGrp.forkproof · cited by 0
- NormedAddGroupHom.ker_completionstatement and proof · cited by 0
- NormedAddGroupHom.ker_zerostatement · cited by 0