Newton's Second Law

F = m * a can be made both as a computational function and as a rewriting lemma.

def SI.secondLaw (m : Mass) (a : Acceleration) : Force

Computational version: obtain force from mass and acceleration.

Equations

• SI.secondLaw m a = m * a

@[reducible, inline]

abbrev SI.F_of (m : Mass) (a : Acceleration) : Force

Convenient alias: F_of looks more "function-like."

Equations

• SI.F_of m a = SI.secondLaw m a

@[simp]

theorem SI.newton_second_law (m : Mass) (a : Acceleration) : F_of m a = m * a

Rewriting version (law equation): rewrite F into m * a. Useful when the problem states Newton's second law.