module module

`IndisputableMonolith.Gravity.Analysis.BlochCellSum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly module_import

declarations in this module (16)

lemma exp_ratio_pow_card L68
lemma exp_ratio_eq_one_iff L82
lemma exp_term_eq_pow L105
theorem expSum_eq_zero L115
theorem expSum_eq_card L137
lemma sum_cos_of_sum_exp_eq_zero L168
theorem cosSum_eq_zero L193
def theta L216
lemma theta_two_mul L222
lemma sum_mul_sum_prod L230
theorem cellSum_exp_eq_prod L238
theorem cellSum_cos_eq_zero L307
theorem cos_mul_cos L321
theorem cellSum_cos_mul_cos L334
theorem eventually_nonaliased L381
theorem cellSum_cos_sq_three_axis L397