Documentation Verification Report

Quotient

📁 Source: Mathlib/Analysis/Normed/Group/Quotient.lean

Statistics

Metric	Count
Definitions `normedMk`, `quotientIsometryEquivOfEq`, `normedAlgebra`, `normedCommRing`, `semiNormedCommRing`, `IsQuotient`, `addGroupSeminorm`, `instNorm`, `instNormedAddCommGroup`, `instSeminormedAddCommGroup`, `quotientBotIsometryEquiv`, `quotientQuotientIsometryEquivQuotient`, `groupSeminorm`, `instNorm`, `instNormedCommGroup`, `instSeminormedCommGroup`, `quotientBotIsometryEquiv`, `quotientQuotientIsometryEquivQuotient`, `quotientIsometryEquivOfEq`, `normedAddCommGroup`, `normedSpace`, `seminormedAddCommGroup`, `quotLIEOfEq`, `quotientQuotientLIEQuotient`, `quotientQuotientLIEQuotientSup`	25
Theorems `ker_normedMk`, `norm_normedMk`, `norm_normedMk_le`, `norm_trivial_quotient_mk`, `apply`, `surjective_normedMk`, `norm_mk_le`, `norm_mk_lt`, `norm`, `norm_le`, `norm_lift`, `surjective`, `isQuotientQuotient`, `lift_mk`, `lift_normNoninc`, `lift_norm_le`, `lift_unique`, `norm_lift_le`, `exists_norm_add_lt`, `exists_norm_mk_lt`, `le_norm_iff`, `nhds_zero_hasBasis`, `norm_eq_addGroupSeminorm`, `norm_eq_infDist`, `norm_lift_apply_le`, `norm_lt_iff`, `norm_mk`, `norm_mk_eq_zero`, `norm_mk_eq_zero_iff_mem_closure`, `norm_mk_le_norm`, `exists_norm_mk_lt`, `exists_norm_mul_lt`, `le_norm_iff`, `nhds_one_hasBasis`, `norm_eq_groupSeminorm`, `norm_eq_infDist`, `norm_lt_iff`, `norm_mk`, `norm_mk_eq_zero`, `norm_mk_eq_zero_iff_mem_closure`, `norm_mk_le_norm`, `completeSpace`, `instIsBoundedSMul`, `norm_mk_le`, `norm_mk_lt`, `quotient_norm_add_le`, `quotient_norm_mk_eq`	47
Total	72

AddSubgroup

Definitions

Name	Category	Theorems
`normedMk` 📖	CompOp	8 math math: `norm_normedMk_le`, `NormedAddGroupHom.lift_mk`, `norm_trivial_quotient_mk`, `surjective_normedMk`, `ker_normedMk`, `NormedAddGroupHom.isQuotientQuotient`, `norm_normedMk`, `normedMk.apply`
`quotientIsometryEquivOfEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_normedMk` 📖	mathematical	—	`NormedAddGroupHom.ker` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `normedMk`	—	`QuotientAddGroup.ker_mk'` `normal_of_comm`
`norm_normedMk` 📖	mathematical	—	`Norm.norm` `NormedAddGroupHom` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `NormedAddGroupHom.hasOpNorm` `normedMk` `Real` `Real.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_antisymm` `norm_normedMk_le` `LE.le.lt_of_ne'` `norm_nonneg` `QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure` `Set.nonempty_compl` `le_mul_iff_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `QuotientAddGroup.norm_lift_apply_le` `normal_of_comm` `QuotientAddGroup.eq_zero_iff`
`norm_normedMk_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddGroupHom` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `NormedAddGroupHom.hasOpNorm` `normedMk` `Real.instOne`	—	`NormedAddGroupHom.opNorm_le_bound` `zero_le_one` `Real.instZeroLEOneClass` `one_mul`
`norm_trivial_quotient_mk` 📖	mathematical	`SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSetLike` `topologicalClosure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.univ`	`Norm.norm` `NormedAddGroupHom` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `NormedAddGroupHom.hasOpNorm` `normedMk` `Real` `Real.instZero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_antisymm` `NormedAddGroupHom.opNorm_le_bound` `le_rfl` `ker_normedMk` `SetLike.mem_coe` `QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure` `MulZeroClass.zero_mul` `norm_nonneg`
`surjective_normedMk` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `DFunLike.coe` `NormedAddGroupHom` `QuotientAddGroup.instSeminormedAddCommGroup` `NormedAddGroupHom.funLike` `normedMk`	—	`Quot.mk_surjective`

AddSubgroup.normedMk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	mathematical	—	`DFunLike.coe` `NormedAddGroupHom` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `NormedAddGroupHom.funLike` `AddSubgroup.normedMk` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoidHom.instFunLike` `QuotientAddGroup.mk'`	—	—

Ideal.Quotient

Definitions

Name	Category	Theorems
`normedAlgebra` 📖	CompOp	—
`normedCommRing` 📖	CompOp	—
`semiNormedCommRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_mk_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `Ideal.instHasQuotient` `SeminormedAddCommGroup.toNorm` `Submodule.Quotient.seminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `SeminormedRing.toNorm`	—	`QuotientAddGroup.norm_mk_le_norm`
`norm_mk_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `ring` `Ideal.instIsTwoSided_1` `SeminormedCommRing.toCommRing` `RingHom.instFunLike` `Norm.norm` `SeminormedRing.toNorm` `Real.instAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `SeminormedAddCommGroup.toNorm` `Submodule.Quotient.seminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Semiring.toModule`	—	`QuotientAddGroup.exists_norm_mk_lt`

NormedAddGroupHom

Definitions

Name	Category	Theorems
`IsQuotient` 📖	CompData	2 math math: `SemiNormedGrp.isQuotient_explicitCokernelπ`, `isQuotientQuotient`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isQuotientQuotient` 📖	mathematical	—	`IsQuotient` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `AddSubgroup.normedMk`	—	`AddSubgroup.surjective_normedMk` `AddSubgroup.ker_normedMk` `quotient_norm_mk_eq`
`lift_mk` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `lift` `AddSubgroup.normedMk`	—	—
`lift_normNoninc` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormNoninc`	`HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `lift`	—	`NormNoninc.normNoninc_iff_norm_le_one` `one_mul` `le_of_opNorm_le` `lift_norm_le`
`lift_norm_le` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instLE` `Norm.norm` `hasOpNorm` `NNReal.toReal`	`HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `lift`	—	`LE.le.trans` `norm_lift_le`
`lift_unique` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `comp` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `AddSubgroup.normedMk`	`lift`	—	`ext` `AddSubgroup.surjective_normedMk`
`norm_lift_le` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instSeminormedAddCommGroup` `hasOpNorm` `lift`	—	`opNorm_le_bound` `norm_nonneg` `QuotientAddGroup.norm_lift_apply_le`

NormedAddGroupHom.IsQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm` 📖	mathematical	`NormedAddGroupHom.IsQuotient`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike` `InfSet.sInf` `Real` `Real.instInfSet` `Set.image` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instSetLike` `NormedAddGroupHom.ker`	—	—
`norm_le` 📖	mathematical	`NormedAddGroupHom.IsQuotient`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike`	—	`norm` `csInf_le` `norm_nonneg` `AddSubgroup.zero_mem` `add_zero`
`norm_lift` 📖	mathematical	`NormedAddGroupHom.IsQuotient` `Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instAdd`	—	`surjective` `Set.image_nonempty` `AddSubgroup.zero_mem` `Real.lt_sInf_add_pos` `map_add` `AddMonoidHomClass.toAddHomClass` `NormedAddGroupHom.toAddMonoidHomClass` `NormedAddGroupHom.mem_ker` `add_zero` `norm`
`surjective` 📖	mathematical	`NormedAddGroupHom.IsQuotient`	`DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike`	—	—

QuotientAddGroup

Definitions

Name	Category	Theorems
`addGroupSeminorm` 📖	CompOp	1 math math: `norm_eq_addGroupSeminorm`
`instNorm` 📖	CompOp	29 math math: `exists_norm_mk_lt`, `le_norm_iff`, `norm_mk_eq_zero_iff_mem_closure`, `AddCircle.norm_div_natCast`, `norm_lt_iff`, `AddCircle.exists_norm_nsmul_le`, `norm_eq_infDist`, `AddCircle.norm_coe_mul`, `AddCircle.norm_half_period_eq`, `norm_mk`, `quotient_norm_add_le`, `AddCircle.exists_norm_eq_of_isOfFinAddOrder`, `nhds_zero_hasBasis`, `UnitAddCircle.mem_approxAddOrderOf_iff`, `AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder`, `quotient_norm_mk_eq`, `AddCircle.norm_coe_eq_abs_iff`, `norm_lift_apply_le`, `norm_mk_eq_zero`, `AddCircle.norm_neg_period`, `UnitAddCircle.norm_eq`, `AddCircle.norm_le_half_period`, `norm_eq_addGroupSeminorm`, `UnitAddCircle.mem_addWellApproximable_iff`, `norm_mk_le_norm`, `AddCircle.norm_eq`, `exists_norm_add_lt`, `AddCircle.norm_eq'`, `AddCircle.norm_eq_of_zero`
`instNormedAddCommGroup` 📖	CompOp	—
`instSeminormedAddCommGroup` 📖	CompOp	21 math math: `AddSubgroup.norm_normedMk_le`, `AddCircle.coe_real_preimage_closedBall_eq_iUnion`, `NormedAddGroupHom.lift_mk`, `AddSubgroup.norm_trivial_quotient_mk`, `NormedAddGroupHom.lift_normNoninc`, `AddCircle.instIsUnifLocDoublingMeasureRealVolume`, `AddCircle.volume_closedBall`, `AddCircle.coe_real_preimage_closedBall_inter_eq`, `UnitAddCircle.mem_approxAddOrderOf_iff`, `AddCircle.closedBall_eq_univ_of_half_period_le`, `AddSubgroup.surjective_normedMk`, `AddCircle.coe_real_preimage_closedBall_period_zero`, `AddCircle.addWellApproximable_ae_empty_or_univ`, `AddSubgroup.ker_normedMk`, `NormedAddGroupHom.lift_norm_le`, `NormedAddGroupHom.norm_lift_le`, `UnitAddCircle.mem_addWellApproximable_iff`, `NormedAddGroupHom.isQuotientQuotient`, `AddSubgroup.norm_normedMk`, `AddCircle.closedBall_ae_eq_ball`, `AddSubgroup.normedMk.apply`
`quotientBotIsometryEquiv` 📖	CompOp	—
`quotientQuotientIsometryEquivQuotient` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_norm_add_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Real.instAdd` `HasQuotient.Quotient` `instHasQuotientAddSubgroup` `instNorm` `DFunLike.coe` `AddMonoidHom` `Quotient.addGroup` `AddSubgroup.normal_of_comm` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoidHom.instFunLike` `mk'`	—	`AddSubgroup.normal_of_comm` `exists_norm_mk_lt` `eq` `add_neg_cancel_left`
`exists_norm_mk_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instAdd` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `instNorm`	—	`norm_lt_iff` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`le_norm_iff` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `SeminormedAddCommGroup.toNorm`	—	`Metric.le_infDist` `dist_zero`
`nhds_zero_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `Real` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Quotient.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Real.instLT` `Real.instZero` `setOf` `Norm.norm` `instNorm`	—	`Set.ext` `ball_zero_eq` `Set.mem_setOf_eq` `norm_lt_iff` `Set.mem_image` `AddSubgroup.normal_of_comm` `mk_zero` `nhds_eq` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.HasBasis.map` `Metric.nhds_basis_ball`
`norm_eq_addGroupSeminorm` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `DFunLike.coe` `AddGroupSeminorm` `Quotient.addGroup` `AddSubgroup.normal_of_comm` `SeminormedAddCommGroup.toAddCommGroup` `Real` `AddGroupSeminorm.funLike` `addGroupSeminorm`	—	—
`norm_eq_infDist` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `Metric.infDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `setOf`	—	—
`norm_lift_apply_le` 📖	mathematical	`DFunLike.coe` `NormedAddGroupHom` `NormedAddGroupHom.funLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `lift` `NormedAddGroupHom.toAddMonoidHom` `Real.instMul` `NormedAddGroupHom.hasOpNorm` `instNorm`	—	`LE.le.eq_or_lt'` `norm_nonneg` `AddSubgroup.normal_of_comm` `mk_surjective` `MulZeroClass.zero_mul` `NormedAddGroupHom.le_opNorm` `not_lt` `lt_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_lt_iff` `LT.lt.not_ge`
`norm_lt_iff` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `SeminormedAddCommGroup.toNorm`	—	`Metric.infDist_lt_iff` `dist_zero`
`norm_mk` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `Metric.infDist` `SeminormedAddCommGroup.toPseudoMetricSpace` `SetLike.coe` `AddSubgroup.instSetLike`	—	`norm_eq_infDist` `NormedAddGroup.to_isIsometricVAdd_left` `NormedAddGroup.to_isIsometricVAdd_right` `Metric.infDist_image` `IsometryEquiv.isometry` `IsometryEquiv.preimage_symm` `sub_zero` `AddSubgroup.normal_of_comm` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `neg_eq_zero` `eq_zero_iff`
`norm_mk_eq_zero` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `Real` `Real.instZero` `SetLike.instMembership` `AddSubgroup.instSetLike`	—	`norm_mk_eq_zero_iff_mem_closure` `IsClosed.closure_eq` `SetLike.mem_coe`
`norm_mk_eq_zero_iff_mem_closure` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `Real` `Real.instZero` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SetLike.coe` `AddSubgroup.instSetLike`	—	`Metric.mem_closure_iff_infDist_zero` `AddSubgroup.zero_mem`
`norm_mk_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `instHasQuotientAddSubgroup` `instNorm` `SeminormedAddCommGroup.toNorm`	—	`LE.le.trans_eq` `Metric.infDist_le_dist_of_mem` `dist_zero_left`

QuotientGroup

Definitions

Name	Category	Theorems
`groupSeminorm` 📖	CompOp	1 math math: `norm_eq_groupSeminorm`
`instNorm` 📖	CompOp	11 math math: `norm_mk`, `norm_mk_eq_zero`, `norm_mk_eq_zero_iff_mem_closure`, `nhds_one_hasBasis`, `exists_norm_mk_lt`, `exists_norm_mul_lt`, `norm_eq_infDist`, `le_norm_iff`, `norm_eq_groupSeminorm`, `norm_lt_iff`, `norm_mk_le_norm`
`instNormedCommGroup` 📖	CompOp	—
`instSeminormedCommGroup` 📖	CompOp	—
`quotientBotIsometryEquiv` 📖	CompOp	—
`quotientQuotientIsometryEquivQuotient` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_norm_mk_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `Norm.norm` `SeminormedCommGroup.toNorm` `Real.instAdd` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `instNorm`	—	`norm_lt_iff` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`exists_norm_mul_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Norm.norm` `SeminormedCommGroup.toNorm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instAdd` `HasQuotient.Quotient` `instHasQuotientSubgroup` `instNorm` `DFunLike.coe` `MonoidHom` `Quotient.group` `Subgroup.normal_of_comm` `SeminormedCommGroup.toCommGroup` `MonoidHom.instFunLike` `mk'`	—	`Subgroup.normal_of_comm` `exists_norm_mk_lt` `mul_inv_cancel_left`
`le_norm_iff` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `SeminormedCommGroup.toNorm`	—	`Metric.le_infDist` `dist_one`
`nhds_one_hasBasis` 📖	mathematical	—	`Filter.HasBasis` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `Real` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Quotient.commGroup` `SeminormedCommGroup.toCommGroup` `Real.instLT` `Real.instZero` `setOf` `Norm.norm` `instNorm`	—	`Set.ext` `ball_one_eq` `Set.mem_setOf_eq` `norm_lt_iff` `Set.mem_image` `Subgroup.normal_of_comm` `mk_one` `nhds_eq` `IsTopologicalGroup.toContinuousMul` `SeminormedCommGroup.toIsTopologicalGroup` `Filter.HasBasis.map` `Metric.nhds_basis_ball`
`norm_eq_groupSeminorm` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `DFunLike.coe` `GroupSeminorm` `Quotient.group` `Subgroup.normal_of_comm` `SeminormedCommGroup.toCommGroup` `Real` `GroupSeminorm.funLike` `groupSeminorm`	—	—
`norm_eq_infDist` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `Metric.infDist` `SeminormedCommGroup.toPseudoMetricSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `SeminormedCommGroup.toCommGroup` `setOf`	—	—
`norm_lt_iff` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `SeminormedCommGroup.toNorm`	—	`Metric.infDist_lt_iff` `dist_one`
`norm_mk` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `Metric.infDist` `SeminormedCommGroup.toPseudoMetricSpace` `SetLike.coe` `Subgroup.instSetLike`	—	`norm_eq_infDist` `NormedGroup.to_isIsometricSMul_left` `NormedGroup.to_isIsometricSMul_right` `Metric.infDist_image` `IsometryEquiv.isometry` `IsometryEquiv.preimage_symm` `div_one` `Subgroup.normal_of_comm` `RightCancelSemigroup.toIsRightCancelMul`
`norm_mk_eq_zero` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `Real` `Real.instZero` `SetLike.instMembership` `Subgroup.instSetLike`	—	`norm_mk_eq_zero_iff_mem_closure` `IsClosed.closure_eq` `SetLike.mem_coe`
`norm_mk_eq_zero_iff_mem_closure` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `Real` `Real.instZero` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SetLike.coe` `Subgroup.instSetLike`	—	`Metric.mem_closure_iff_infDist_zero` `Subgroup.one_mem`
`norm_mk_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `instHasQuotientSubgroup` `instNorm` `SeminormedCommGroup.toNorm`	—	`LE.le.trans_eq` `Metric.infDist_le_dist_of_mem` `dist_one_left`

Subgroup

Definitions

Name	Category	Theorems
`quotientIsometryEquivOfEq` 📖	CompOp	—

Submodule

Definitions

Name	Category	Theorems
`quotLIEOfEq` 📖	CompOp	—
`quotientQuotientLIEQuotient` 📖	CompOp	—
`quotientQuotientLIEQuotientSup` 📖	CompOp	—

Submodule.Quotient

Definitions

Name	Category	Theorems
`normedAddCommGroup` 📖	CompOp	—
`normedSpace` 📖	CompOp	—
`seminormedAddCommGroup` 📖	CompOp	6 math math: `instIsBoundedSMul`, `completeSpace`, `Ideal.Quotient.norm_mk_lt`, `norm_mk_le`, `norm_mk_lt`, `Ideal.Quotient.norm_mk_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.hasQuotient` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `seminormedAddCommGroup`	—	`QuotientAddGroup.completeSpace_right` `IsUniformAddGroup.isRightUniformAddGroup` `SeminormedAddCommGroup.to_isUniformAddGroup` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `AddSubgroup.normal_of_comm`
`instIsBoundedSMul` 📖	mathematical	—	`IsBoundedSMul` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.hasQuotient` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `seminormedAddCommGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalSeminormedCommRing.toNonUnitalCommRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `instZeroQuotient` `instSMul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Module.toDistribMulAction`	—	`IsBoundedSMul.of_norm_smul_le` `le_of_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.HasBasis.tendsto_iff` `Metric.nhds_basis_ball` `Continuous.tendsto` `UniformContinuous.continuous` `Real.uniformContinuous_const_mul` `norm_mk_lt` `LE.le.trans` `norm_mk_le` `norm_smul_le` `LT.lt.le` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`norm_mk_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.hasQuotient` `SeminormedAddCommGroup.toNorm` `seminormedAddCommGroup`	—	`QuotientAddGroup.norm_mk_le_norm`
`norm_mk_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`SeminormedAddCommGroup.toAddCommGroup` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instAdd` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `seminormedAddCommGroup`	—	`QuotientAddGroup.exists_norm_mk_lt`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotient_norm_add_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Real.instAdd`	—	`norm_add_le`
`quotient_norm_mk_eq` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `QuotientAddGroup.instNorm` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `SeminormedAddCommGroup.toAddCommGroup` `AddMonoidHom.instFunLike` `QuotientAddGroup.mk'` `InfSet.sInf` `Real` `Real.instInfSet` `Set.image` `SeminormedAddCommGroup.toNorm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `AddSubgroup.instSetLike`	—	`AddSubgroup.normal_of_comm` `QuotientAddGroup.mk'_apply` `sInf_image'` `Metric.infDist_image` `isometry_neg` `NormedAddGroup.to_isIsometricVAdd_left` `NormedAddGroup.to_isIsometricVAdd_right` `Set.image_neg_eq_neg` `neg_coe_set` `AddSubgroupClass.toNegMemClass` `AddSubgroup.instAddSubgroupClass` `Metric.infDist_eq_iInf` `dist_eq_norm'` `sub_neg_eq_add` `add_comm`

---

← Back to Index