Theorems · Definition · functional analysis
AddSubgroup.normedMk
{M : Type u_1} → [inst : SeminormedAddCommGroup M] → (S : AddSubgroup M) → NormedAddGroupHom M (M ⧸ S)The morphism from a seminormed group to the quotient by a subgroup.
- Defined in
- Mathlib.Analysis.Normed.Group.Quotient
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddSubgroupstatement and proof · cited by 3,232
- AddMonoidHomproof · cited by 3,230
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- HasQuotient.Quotientstatement and proof · cited by 2,301
- NormedAddGroupHomstatement · cited by 216
- ZeroHom.toFunproof · cited by 101
- AddMonoidHom.toZeroHomproof · cited by 61
- QuotientAddGroup.mk'proof · cited by 60
Cited by11
Results whose statement or proof uses this declaration.
- SemiNormedGrp.cokernelCoconeproof · cited by 5
- AddSubgroup.surjective_normedMkstatement · cited by 2
- AddSubgroup.ker_normedMkstatement · cited by 2
- NormedAddGroupHom.isQuotientQuotientstatement · cited by 1
- AddSubgroup.norm_normedMk_lestatement and proof · cited by 1
- AddSubgroup.normedMk.applystatement · cited by 0
- AddSubgroup.norm_normedMkstatement and proof · cited by 0
- AddSubgroup.norm_trivial_quotient_mkstatement and proof · cited by 0
- NormedAddGroupHom.lift_mkstatement · cited by 0
- NormedAddGroupHom.lift_uniquestatement and proof · cited by 0
- SemiNormedGrp₁.cokernelCoconeproof · cited by 0