Documentation Verification Report

LeftRegular

📁 Source: ClassFieldTheory/Cohomology/LeftRegular.lean

Statistics

Metric	Count
Definitions `norm`, `norm'`, `res_norm`, `res_norm'`, `H0trivial`	5
Theorems `H0Iso_res_norm`, `groupCoh_map_res_norm`, `res_span_norm`, `res_span_norm'`, `span_norm`, `span_norm'`, `zeroι_norm`, `zeroι_res_norm`, `map_comp_H0trivial`, `map_comp_H0trivial_apply`	10
Total	15

Rep.leftRegular

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	2 math math: `span_norm`, `zeroι_norm`
`norm'` 📖	CompOp	1 math math: `span_norm'`
`res_norm` 📖	CompOp	4 math math: `zeroι_res_norm`, `H0Iso_res_norm`, `res_span_norm`, `groupCoh_map_res_norm`
`res_norm'` 📖	CompOp	2 math math: `H0Iso_res_norm`, `res_span_norm'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`H0Iso_res_norm` 📖	mathematical	—	`Rep.res` `res_norm` `res_norm'`	—	—
`groupCoh_map_res_norm` 📖	mathematical	—	`Rep.res` `ε` `res_norm` `groupCohomology.H0trivial`	—	`groupCohomology.map_comp_H0trivial` `zeroι_res_norm`
`res_span_norm` 📖	mathematical	—	`Rep.res` `res_norm`	—	`res_span_norm'`
`res_span_norm'` 📖	mathematical	—	`Rep.res` `res_norm'`	—	`of_apply`
`span_norm` 📖	mathematical	—	`norm`	—	`norm.eq_1` `span_norm'`
`span_norm'` 📖	mathematical	—	`norm'`	—	—
`zeroι_norm` 📖	mathematical	—	`RepresentationTheory.groupCohomology.zeroι` `norm` `of`	—	—
`zeroι_res_norm` 📖	mathematical	—	`Rep.res` `RepresentationTheory.groupCohomology.zeroι` `res_norm` `of`	—	`H0Iso_res_norm`

groupCohomology

Definitions

Name	Category	Theorems
`H0trivial` 📖	CompOp	3 math math: `map_comp_H0trivial`, `Rep.leftRegular.groupCoh_map_res_norm`, `map_comp_H0trivial_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_comp_H0trivial` 📖	mathematical	—	`H0trivial` `RepresentationTheory.groupCohomology.zeroι`	—	—
`map_comp_H0trivial_apply` 📖	mathematical	—	`H0trivial` `RepresentationTheory.groupCohomology.zeroι`	—	`map_comp_H0trivial`

---

← Back to Index