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,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,147 to 1,152 of 2,569 results.
frequently_in_finite_set
Mathematical statement
Note that only the → direction needs the finiteness assumption.
Source project: Automata Theory
Person-level attribution pending.
FreyCurve.j_valuation_of_bad_prime
Mathematical statement
The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
Mathematical statement
Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package.
Source project: Fermat's Last Theorem
Person-level attribution pending.
FromMathlib.inj_on_of_nodup_map
Mathematical statement
NB. Copied from Mathlib
Source project: Iris-Lean
Person-level attribution pending.
FTheory.SU5.FiveQuanta.anomalyCoefficient_of_reduce
Project documentation
The anomaly coefficient of a FiveQuanta is given by the pair of integers: (∑ᵢ qᵢ Nᵢ, ∑ᵢ qᵢ² Nᵢ). The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly, see equation (23) of arXiv:1401.5084. -/ def anomalyCoefficient (F : FiveQuanta 𝓩) : 𝓩 × 𝓩 := ((F...
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FiveQuanta.decompose_filter_charge
Project documentation
The decomposition of a FiveQuanta into a FiveQuanta which has the same reduce by has fluxes ⟨1, -1⟩ and ⟨0,1⟩ only. -/ def decompose (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.bind fun p => (decomposeFluxes p.2).map fun f => (p.1, f) /-! #### C.2.1. Decomposition distributes over addition -/ lemma decompose_add (x y : FiveQuanta 𝓩) : (x + y).deco...
Source project: Physlib
Person-level attribution pending.