TimeUnit

📁 Source: PhysLean/SpaceAndTime/Time/TimeUnit.lean

Statistics

Metric	Count
Definitions TimeUnit, centiseconds, days, deciseconds, femtoseconds, hours, instHDivNNReal, instInhabited, microseconds, milliseconds, minutes, nanoseconds, picoseconds, scale, seconds, val, weeks	17
Theorems days_div_hours, days_div_minutes, days_div_seconds, div_eq_val, div_mul_div_coe, div_neq_zero, div_pos, div_self, div_symm, hours_div_seconds, minutes_div_seconds, property, scale_div_scale, scale_div_self, scale_one, scale_scale, self_div_scale, val_neq_zero, val_pos, weeks_div_hours, weeks_div_minutes, weeks_div_seconds	22
Total	39

TimeUnit

Definitions

Name	Category	Theorems
centiseconds 📖	CompOp	—
days 📖	CompOp	3 math math: days_div_minutes, days_div_seconds, days_div_hours
deciseconds 📖	CompOp	—
femtoseconds 📖	CompOp	—
hours 📖	CompOp	3 math math: weeks_div_hours, hours_div_seconds, days_div_hours
instHDivNNReal 📖	CompOp	18 math math: minutes_div_seconds, weeks_div_minutes, days_div_minutes, self_div_scale, div_neq_zero, UnitChoices.dimScale_apply, div_symm, div_pos, weeks_div_seconds, weeks_div_hours, div_mul_div_coe, scale_div_scale, hours_div_seconds, days_div_seconds, days_div_hours, div_eq_val, scale_div_self, div_self
instInhabited 📖	CompOp	—
microseconds 📖	CompOp	—
milliseconds 📖	CompOp	—
minutes 📖	CompOp	3 math math: minutes_div_seconds, weeks_div_minutes, days_div_minutes
nanoseconds 📖	CompOp	—
picoseconds 📖	CompOp	—
scale 📖	CompOp	5 math math: scale_one, self_div_scale, scale_div_scale, scale_scale, scale_div_self
seconds 📖	CompOp	5 math math: minutes_div_seconds, weeks_div_seconds, hours_div_seconds, days_div_seconds, UnitChoices.SI_time
val 📖	CompOp	6 math math: TimeTransMan.addTime_val, property, val_pos, TimeTransMan.diff_eq_val, TimeTransMan.addTime_eq_val, div_eq_val
weeks 📖	CompOp	3 math math: weeks_div_minutes, weeks_div_seconds, weeks_div_hours

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
days_div_hours 📖	mathematical	—	TimeUnit instHDivNNReal days hours	—	scale_div_scale div_self
days_div_minutes 📖	mathematical	—	TimeUnit instHDivNNReal days minutes	—	scale_div_scale div_self
days_div_seconds 📖	mathematical	—	TimeUnit instHDivNNReal days seconds	—	scale_div_self
div_eq_val 📖	mathematical	—	TimeUnit instHDivNNReal val val_pos	—	—
div_mul_div_coe 📖	mathematical	—	TimeUnit instHDivNNReal	—	—
div_neq_zero 📖	mathematical	—	TimeUnit instHDivNNReal	—	val_pos div_eq_val
div_pos 📖	mathematical	—	TimeUnit instHDivNNReal	—	div_neq_zero
div_self 📖	mathematical	—	TimeUnit instHDivNNReal	—	val_pos val_neq_zero
div_symm 📖	mathematical	—	TimeUnit instHDivNNReal	—	val_pos div_eq_val
hours_div_seconds 📖	mathematical	—	TimeUnit instHDivNNReal hours seconds	—	scale_div_self
minutes_div_seconds 📖	mathematical	—	TimeUnit instHDivNNReal minutes seconds	—	scale_div_self
property 📖	mathematical	—	val	—	—
scale_div_scale 📖	mathematical	—	TimeUnit instHDivNNReal scale	—	—
scale_div_self 📖	mathematical	—	TimeUnit instHDivNNReal scale	—	val_pos
scale_one 📖	mathematical	—	scale	—	—
scale_scale 📖	mathematical	—	scale	—	—
self_div_scale 📖	mathematical	—	TimeUnit instHDivNNReal scale	—	val_pos
val_neq_zero 📖	—	—	—	—	property
val_pos 📖	mathematical	—	val	—	property
weeks_div_hours 📖	mathematical	—	TimeUnit instHDivNNReal weeks hours	—	scale_div_scale div_self
weeks_div_minutes 📖	mathematical	—	TimeUnit instHDivNNReal weeks minutes	—	scale_div_scale div_self
weeks_div_seconds 📖	mathematical	—	TimeUnit instHDivNNReal weeks seconds	—	scale_div_self

(root)

Definitions

Name	Category	Theorems
TimeUnit 📖	CompData	18 math math: TimeUnit.minutes_div_seconds, TimeUnit.weeks_div_minutes, TimeUnit.days_div_minutes, TimeUnit.self_div_scale, TimeUnit.div_neq_zero, UnitChoices.dimScale_apply, TimeUnit.div_symm, TimeUnit.div_pos, TimeUnit.weeks_div_seconds, TimeUnit.weeks_div_hours, TimeUnit.div_mul_div_coe, TimeUnit.scale_div_scale, TimeUnit.hours_div_seconds, TimeUnit.days_div_seconds, TimeUnit.days_div_hours, TimeUnit.div_eq_val, TimeUnit.scale_div_self, TimeUnit.div_self

---

← Back to Index