WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Circular motion

Revision #2375 → #3024 · back to history

modifiedCentripetal acceleration from changing velocity directionc35e8f6a53a8
FieldFrom #2375To #3024
noteCentripetal force/acceleration is a physics concept absent from Mathlib (loogle finds no `centripetal` decls).Centripetal force/acceleration is a physics concept absent from Mathlib.
modifiedAngular velocity from perioda6e216572130
FieldFrom #2375To #3024
noteThe relation ω = 2π/T is a physics definition not present in Mathlib (no `angularVelocity` decls).The relation ω = 2π/T is a physics definition not present in Mathlib.
addedVelocity magnitude equals ω rc4797d219e46
addedAcceleration magnitude equals ω² r opposite to r(t)3519408769b0
addedRadial component of velocity vanishes for constant-radius motion9a49eba759a0