Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersRep.isZero_ofEven_odd
Plain-language statement
Let M be a representation of a finite cyclic group G. Suppose there are even and positive integers e and o with e even and o odd, such that Hᵉ(G,M) and Hᵒ(G,M) are both zero. Then Hⁿ(G,M) is zero for all n > 0.
Source project: Class Field Theory
Person-level attribution pending.
Rep.map₁_comp_ind₁'_iso_coind₁'
Plain-language statement
Let M be a representation of a finite cyclic group G. Then the following square commutes coind₁'.obj M -------> coind₁'.obj M | | | | ↓ ↓ ind₁'.obj M -------> ind₁'.obj M The vertical maps are the canonical isomorphism ind₁'_iso_coind₁ and the horizontal maps are map₁ and map₂.
Source project: Class Field Theory
Person-level attribution pending.