pairingDual_apply_apply_eq_one — Mathlib

English

If a and f satisfy f_i(x_i)=1 and f_i(x_j)=0 for i ≠ j, then for any n and a (order-embedding ι), pairingDual applied to ιMulti(f∘a) and ιMulti(x∘a) equals 1.

Русский

Если для всех i выполняются f_i(x_i)=1 и f_i(x_j)=0 при i≠j, то для любых n и вложения a, pairingDual(ιMulti(f∘a), ιMulti(x∘a)) = 1.

LaTeX

$$$ pairingDual\ R\ M\ n (ιMulti\ _\ _ (f \circ a)) (ιMulti\ _\ _ (x \circ a)) = 1 $$$

Lean4

theorem pairingDual_apply_apply_eq_one (a : Fin n ↪o ι) :
    pairingDual R M n (ιMulti _ _ (f ∘ a)) (ιMulti _ _ (x ∘ a)) = 1 :=
  by
  simp only [pairingDual_ιMulti_ιMulti, Function.comp_apply]
  rw [← Matrix.det_one (n := Fin n)]
  congr
  ext i j
  dsimp
  by_cases hij : i = j
  · subst hij
    simp only [h₁, Matrix.one_apply_eq]
  · rw [h₀ (by simpa using Ne.symm hij), Matrix.one_apply_ne hij]

Похожие утверждения