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 filtersCKMMatrix.VAbs_sum_sq_row_eq_one
Plain-language statement
The absolute value squared of any row of a CKM matrix is 1, in terms of Vabs.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.acceleration_eq_of_equationOfMotion
Plain-language statement
Solving the equation of motion for the acceleration: along a solution the second derivative is -(k/m) x - (γ/m) ẋ.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.equationOfMotion_unique
Plain-language statement
Any two smooth solutions of the damped equation of motion with the same initial position and velocity are equal.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.gradLagrangian_eq_force
Plain-language statement
The variational gradient of the Caldirola–Kanai action is the exponential factor times the difference of the force and mass times acceleration appearing in Newton's second law.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.toUndamped_equationOfMotion
Plain-language statement
When γ = 0, the damped equation of motion is equivalent to the equation of motion for the corresponding undamped harmonic oscillator.
Source project: Physlib
Person-level attribution pending.
ClassicalMechanics.DampedHarmonicOscillator.trajectory_equationOfMotion_of_criticallyDamped
Plain-language statement
In the critically damped regime, the selected trajectory satisfies the damped equation of motion.
Source project: Physlib
Person-level attribution pending.