def
definition
def or abbrev
import_measurements
show as:
view Lean formalization →
formal statement (Lean)
12def import_measurements : List Measurement :=
proof body
Definition body.
13 [
14 { name := "AlphaInvPrediction", value := (137.035999084 : ℝ), error := (0.000000084 : ℝ) },
15 { name := "Sin2ThetaW_at_MZ", value := (0.23121 : ℝ), error := (0.00004 : ℝ) },
16 { name := "AlphaS_at_MZ", value := (0.1179 : ℝ), error := (0.0009 : ℝ) },
17 { name := "ElectronG2", value := (0.00115965218073 : ℝ), error := (2.8e-13 : ℝ) },
18 { name := "MuonG2", value := (0.00116592062 : ℝ), error := (4.1e-10 : ℝ) },
19 { name := "MW_over_MZ", value := (0.88153 : ℝ), error := (0.00018 : ℝ) }
20 ]
21
22end IndisputableMonolith.Data