Documentation Verification Report

NullSubmodule

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

Statistics

Metric	Count
Definitions `nullAddSubgroup`, `nullSubgroup`, `nullSubmodule`	3
Theorems `isClosed_nullAddSubgroup`, `isClosed_nullSubgroup`, `isClosed_nullSubmodule`, `mem_nullAddSubgroup_iff`, `mem_nullSubgroup_iff`, `mem_nullSubmodule_iff`	6
Total	9

(root)

Definitions

Name	Category	Theorems
`nullAddSubgroup` 📖	CompOp	2 math math: `mem_nullAddSubgroup_iff`, `isClosed_nullAddSubgroup`
`nullSubgroup` 📖	CompOp	2 math math: `isClosed_nullSubgroup`, `mem_nullSubgroup_iff`
`nullSubmodule` 📖	CompOp	4 math math: `InnerProductSpace.nullSubmodule_le_ker_toDualMap_left`, `isClosed_nullSubmodule`, `mem_nullSubmodule_iff`, `InnerProductSpace.nullSubmodule_le_ker_toDualMap_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_nullAddSubgroup` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SetLike.coe` `AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddSubgroup.instSetLike` `nullAddSubgroup`	—	`IsClosed.preimage` `continuous_norm` `isClosed_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`
`isClosed_nullSubgroup` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `SetLike.coe` `Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `Subgroup.instSetLike` `nullSubgroup`	—	`IsClosed.preimage` `continuous_norm'` `isClosed_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`
`isClosed_nullSubmodule` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SetLike.coe` `Submodule` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Submodule.setLike` `nullSubmodule`	—	`isClosed_nullAddSubgroup`
`mem_nullAddSubgroup_iff` 📖	mathematical	—	`AddSubgroup` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `nullAddSubgroup` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instZero`	—	—
`mem_nullSubgroup_iff` 📖	mathematical	—	`Subgroup` `SeminormedGroup.toGroup` `SeminormedCommGroup.toSeminormedGroup` `SetLike.instMembership` `Subgroup.instSetLike` `nullSubgroup` `Norm.norm` `SeminormedCommGroup.toNorm` `Real` `Real.instZero`	—	—
`mem_nullSubmodule_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `SeminormedRing.toRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `nullSubmodule` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instZero`	—	—

---

← Back to Index