Depth

📁 Source: FLT/Patching/Utils/Depth.lean

Statistics

Metric	Count
Definitions depth	1
Theorems depth_le_dim, depth_le_dim_annihilator, depth_le_krullDim_support, depth_le_of_free, depth_of_isScalarTower, depth_of_subsingleton, faithfulSMul_of_depth_eq_ringKrullDim, length_le_depth, isWeaklyRegular_of_free, isWeaklyRegular_of_free_aux, isWeaklyRegular_of_subsingleton, instSubsingletonQuotientSubmodule_fLT, isSMulRegular_iff_of_free	13
Total	14

Module

Definitions

Name	Category	Theorems
depth 📖	CompOp	7 math math: depth_le_of_free, depth_of_subsingleton, depth_le_dim, depth_of_isScalarTower, length_le_depth, depth_le_dim_annihilator, depth_le_krullDim_support

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
depth_le_dim 📖	mathematical	—	depth	—	depth_le_dim_annihilator
depth_le_dim_annihilator 📖	mathematical	—	depth	—	depth_le_krullDim_support
depth_le_krullDim_support 📖	mathematical	—	depth	—	depth.eq_1 length_le_depth
depth_le_of_free 📖	mathematical	—	depth	—	depth_of_subsingleton RingTheory.Sequence.isWeaklyRegular_of_free
depth_of_isScalarTower 📖	mathematical	—	depth	—	—
depth_of_subsingleton 📖	mathematical	—	depth	—	depth.eq_1 instSubsingletonQuotientSubmodule_fLT
faithfulSMul_of_depth_eq_ringKrullDim 📖	—	depth	—	—	depth_le_dim_annihilator
length_le_depth 📖	mathematical	—	depth	—	—

RingTheory.Sequence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isWeaklyRegular_of_free 📖	—	—	—	—	isWeaklyRegular_of_free_aux
isWeaklyRegular_of_free_aux 📖	—	—	—	—	isSMulRegular_iff_of_free
isWeaklyRegular_of_subsingleton 📖	—	—	—	—	instSubsingletonQuotientSubmodule_fLT

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonQuotientSubmodule_fLT 📖	—	—	—	—	—
isSMulRegular_iff_of_free 📖	—	—	—	—	—

---

← Back to Index