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 121 research declarations. Search 10,000 more complete Mathlib declarations.
121 results
Clear filtersIsNonarchimedeanLocalField.exists_pow_smul_mem_integer
Plain-language statement
Every element of L is carried into the integers 𝒪[L] by a large enough power of a uniformiser of K.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.le_maximalUnramified_iff
Plain-language statement
The maximal unramified subextension is maximal.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_algEquiv_of_isUnramified
Plain-language statement
If L/K is unramified, then L is isomorphic to Kn where n = [L:K].
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_alghom_of_dvd_f
Plain-language statement
If Kn denotes the unramified extension of K of degree n, then Kn embeds into L if n ∣ f K L. This is half of the universal property.
Source project: Class Field Theory
Person-level attribution pending.
log_le_const_mul_pow
Project documentation
The union of B-sets used in the proof of proposition 2.6. -/ noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ)) := (indexSet' α β γ d x ε).sup fun ⟨r, s, t, c⟩ ↦ B_finset d c (fun i ↦ 2^r i) (fun i ↦ 2^s i) (fun i ↦ 2^t i) theorem similar_pow_log {x : ℕ} (hx : 0 < x) : x ~ 2 ^ Na...
Source project: ABC Exceptions
Person-level attribution pending.
MaximalPQuotient.isPGroup_of_isTorsion
Plain-language statement
The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group.
Source project: Fermat's Last Theorem
Person-level attribution pending.