English
In crystallographic data, for i in the base’s support, ω(b) e_i = f_i ω(b).
Русский
В кристаллографических данных выполняется соотношение ω(b) e_i = f_i ω(b) для i из поддержки базиса.
LaTeX
$$$ \\omega b \\cdot e i = f i \\cdot \\omega b $$$
Lean4
theorem ω_mul_e [Fintype ι] (i : b.support) : ω b * e i = f i * ω b :=
by
letI := P.indexNeg
classical
ext (k | k) (l | l)
· simp [ω, e, f]
· simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
· simp [ω, e, f]
· simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂,
Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
simp [neg_eq_iff_eq_neg, sub_eq_add_neg]
