theorem
proved
magic_numbers_contain_8
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.NuclearMagicNumbersFromRS on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32theorem magic_2_eq_2pow1 : (2 : ℕ) = 2 ^ 1 := by decide
33
34/-- All magic numbers are in the list. -/
35theorem magic_numbers_contain_8 : 8 ∈ magicNumbers := by decide
36theorem magic_numbers_contain_2 : 2 ∈ magicNumbers := by decide
37
38structure NuclearMagicCert where
39 seven_magic : magicNumbers.card = 7
40 eight_from_8tick : (8 : ℕ) = 2 ^ 3
41 has_8 : 8 ∈ magicNumbers
42 has_2 : 2 ∈ magicNumbers
43
44def nuclearMagicCert : NuclearMagicCert where
45 seven_magic := magicNumbersCard
46 eight_from_8tick := magic_8_eq_2cubed
47 has_8 := magic_numbers_contain_8
48 has_2 := magic_numbers_contain_2
49
50end IndisputableMonolith.Physics.NuclearMagicNumbersFromRS