Documentation

Lean 4 Proof

theorem shareFunction_uniform_at_symmetry {J : ℕ} (hJ : 0 < J)
    {c : ℝ} (hc : c ≠ 0) (j : Fin J) :
    shareFunction (fun _ : Fin J => c) j = 1 / ↑J := by
  simp only [shareFunction, Finset.sum_const, Finset.card_univ,
    Fintype.card_fin, nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:524

Module Section

Ten Views of a Single Object:

In the same file