pith. machine review for the scientific record. sign in
theorem proved term proof

reparam_coefficients_obstruct_degree_two

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)

  52theorem reparam_coefficients_obstruct_degree_two
  53    (c : ℝ) :
  54    ¬ (∀ s : ℝ, reparamDiagonal s = degreeTwoDiagonal c s) := by

proof body

Term-mode proof.

  55  intro h
  56  exact reparam_diagonal_not_degree_two ⟨c, h⟩
  57
  58end LogicAsFunctionalEquation
  59end Foundation
  60end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.