def
hypothesis interface
def or abbrev
SMCancellationHypothesis
show as:
view Lean formalization →
formal statement (Lean)
126def SMCancellationHypothesis (a_gauge a_scalar : ℝ) : Prop :=
proof body
Definition body.
127 a_scalar = -a_gauge
128
129/-- The SM cancellation hypothesis implies the cancellation condition. -/