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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersCslib.Logic.PL.Theory.equiv_iff_equiv_derivableIn_hypothesis
Plain-language statement
A and B are equivalent (in T) iff they have the same strength as hypotheses.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.elimVar_correct
Plain-language statement
Correctness for the elimVar algorithm, which provides the inductive step of the bracket abstraction algorithm. We induct backwards on the list, corresponding to applying the transformation from the inside out. Since we haven't defined reduction for polynomials, we substitute arbitrary terms for the inner variables.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.toSKI_correct
Plain-language statement
Correctness for the toSKI (bracket abstraction) algorithm.
Source project: Lean Computer Science Library
Person-level attribution pending.
dist_affineCombination_le_dist_interleaved₂
Plain-language statement
Lemma: Distance of Affine Combination is Bounded by Interleaved Distance
Source project: ArkLib
Person-level attribution pending.
Electromagnetism.DistElectromagneticPotential.distTensorDeriv_basis_repr_apply
Project documentation
The creation of an electromagnetic potential from a static vector potential. -/ noncomputable def ofStaticVectorPotential {d} (c : SpeedOfLight) : ((Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) →ₗ[ℝ] DistElectromagneticPotential d := ofVectorPotential c ∘ₗ Space.constantTime TODO "Add a constructor for DistElectromagneticPotential from electric and magnetic f...
Source project: Physlib
Person-level attribution pending.
Fin.induction_append_left
Plain-language statement
Fin.induction on m + n for i ≤ m steps is equivalent to Fin.induction on m for i steps.
Source project: ArkLib
Person-level attribution pending.