Main results 201 to 205
| Declaration | Kind | Where | Note |
|---|---|---|---|
ContinuousMap.postcomp_surjective |
theorem | ContinuousGroupCohomology/Topology/ContinuousMap/Exact.lean, line 91 | |
TopRep.coind₁Functor_shortExact |
theorem | ContinuousGroupCohomology/CoinductionExactness.lean, line 53 | |
MonoidAlgebra.finiteFunctionTensorLinearEquiv |
def | ContinuousGroupCohomology/FiniteFunctionTensor.lean, line 50 | |
MonoidAlgebra.finiteFunctionTensorLinearEquiv_naturality |
theorem | ContinuousGroupCohomology/FiniteFunctionTensor.lean, line 112 | |
Representation.finiteFunctionTensorLinearEquiv_twisted |
theorem | ContinuousGroupCohomology/FiniteFunctionTensor.lean, line 138 |
Quoted from the main results in formalization.yaml of FormalFrontier/continuous-group-cohomology at commit 4434e3f2, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.