theorem
proved
term proof
pmns_theta12_born_forced
show as:
view Lean formalization →
formal statement (Lean)
246theorem pmns_theta12_born_forced :
247 sin2_theta12_pred = solar_weight - solar_radiative_correction := by
proof body
Term-mode proof.
248 unfold sin2_theta12_pred
249 rfl
250