theorem
proved
term proof
time_kernel_dimensionless
show as:
view Lean formalization →
formal statement (Lean)
8theorem time_kernel_dimensionless (c T τ : ℝ) (hc : 0 < c) :
9 IndisputableMonolith.Gravity.ILG.w_time_ratio (c * T) (c * τ)
10 = IndisputableMonolith.Gravity.ILG.w_time_ratio T τ := by
proof body
Term-mode proof.
11 simpa using IndisputableMonolith.Gravity.ILG.w_time_ratio_rescale (c:=c) (Tdyn:=T) (τ0:=τ) hc
12
13end TruthCore
14end IndisputableMonolith
15