lemma proved wrapper

`w_t_ref`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  89lemma w_t_ref (P : Params) (τ0 : ℝ) (hτ : τ0 ≠ 0) : w_t P τ0 τ0 = 1 :=

proof body

One-line wrapper that applies w_t_ref_with.

  90  w_t_ref_with defaultConfig defaultConfig_props P τ0 hτ
  91

depends on (8)

Lean names referenced from this declaration's body.

defaultConfig in IndisputableMonolith.Gravity.ILG decl_use
defaultConfig_props in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
w_t in IndisputableMonolith.Gravity.ILG decl_use
w_t_ref_with in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use