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 20 research declarations. Search 10,000 more complete Mathlib declarations.
20 results
Clear filtersPadic.mulValuation_lt_iff_norm_lt
Plain-language statement
Strict comparison of Padic.mulValuation matches strict comparison of the norm.
Source project: Class Field Theory
Person-level attribution pending.
Rep.herbrandQuotient_isNonarchimedeanLocalField_units
Plain-language statement
herbrand quotient of Lˣ is [L:K]
Source project: Class Field Theory
Person-level attribution pending.
Rep.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.
Rep.split.TateTheorem_lemma_1
Plain-language statement
If σ generates H²(G,M) then the map H²(G,M) ⟶ H²(G,split σ) is zero.
Source project: Class Field Theory
Person-level attribution pending.
Rep.split.TateTheorem_lemma_2
Plain-language statement
For any subgroup H of G, the connecting hommorphism in the splitting module long exact sequence H¹(H,aug) ⟶ H²(H,M) is an isomorphism.
Source project: Class Field Theory
Person-level attribution pending.