def
definition
noetherTheoremDeepCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.NoetherTheoremDeep on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
56 energy_nonneg : ∀ r : ℝ, 0 < r → 0 ≤ energy_RS r
57 energy_zero_at_eq : energy_RS 1 = 0
58
59noncomputable def noetherTheoremDeepCert : NoetherTheoremDeepCert where
60 four_charges := four_charges
61 energy_nonneg := energy_nonneg
62 energy_zero_at_eq := energy_zero_at_eq
63
64theorem noetherTheoremDeepCert_inhabited : Nonempty NoetherTheoremDeepCert :=
65 ⟨noetherTheoremDeepCert⟩
66
67end
68end NoetherTheoremDeep
69end Foundation
70end IndisputableMonolith