lemma proved tactic proof

`lambda_0_sq`

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

formal statement (Lean)

  53lemma lambda_0_sq : lambda_0 ^ 2 = 1 / 2 := by

proof body

Tactic-mode proof.

  54  unfold lambda_0
  55  rw [div_pow]
  56  have h2 : (0 : ℝ) ≤ 2 := by norm_num
  57  rw [Real.sq_sqrt h2]
  58  norm_num
  59
  60/-- The balance residual vanishes at lambda_0. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

balance_at_lambda_0 in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
balance_determines_lambda in IndisputableMonolith.Constants.LambdaRecDerivation decl_use

depends on (2)

Lean names referenced from this declaration's body.

lambda_0 in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_0 in IndisputableMonolith.Materials.HydrideSCOptimization decl_use