theorem
proved
term proof
linearized_implies_weak
show as:
view Lean formalization →
formal statement (Lean)
105theorem linearized_implies_weak (h : regime_covered .linearized = true) :
106 regime_covered .weakField = true := by decide
proof body
Term-mode proof.
107
108/-! ## Certificate -/
109