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 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersFluidDynamics.FluidFlow.timeDeriv_smul_velocity
Plain-language statement
Product rule for the time derivative of a scalar field times a velocity field.
Source project: Physlib
Person-level attribution pending.
FluidDynamics.navier_stokes_iff_convective_navier_stokes
Plain-language statement
The conservative and convective Navier-Stokes forms are equivalent when the fields are differentiable enough for the product rules.
Source project: Physlib
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.
FTheory.SU5.FiveQuanta.decompose_toChargeMap
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.
FTheory.SU5.FiveQuanta.decompose_toCharges_dedup
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.