InflationRestriction
📁 Source: ClassFieldTheory/Cohomology/Functors/InflationRestriction.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsinflationRestriction | 1 |
| 3 | |
| Total | 4 |
| 3 |
groupCohomology
Definitions
| Name | Category | Theorems |
|---|---|---|
inflationRestriction 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
inflation_restriction_exact 📖 ⚠️ | mathematical | Rep.res | inflationRestriction | — | — |
inflation_restriction_mono 📖 ⚠️ | mathematical | Rep.res | inflationRestriction | — | — |
quotientToInvariantsFunctor'_shortExact_ofShortExact 📖 ⚠️ | mathematical | Rep.res | Rep.quotientToInvariantsFunctor'Rep.instPreservesZeroMorphismsQuotientToInvariantsFunctor' | — | Rep.instPreservesZeroMorphismsQuotientToInvariantsFunctor' |
---