OAI/Analysis/Mahler/RawAlternatingCalculus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.raw_alternatization_reindex line 12

   Source documentation

   Full alternatization commutes with any explicit slot identification.

   theorem raw_alternatization_reindex
       (a : MultilinearMap ℝ (fun _ : ι => E) ℂ) (e : ι ≃ κ) :
       (a.domDomCongr e).alternatization = a.alternatization.domDomCongr e := by
   …

2. theorem OAI.Mahler.raw_alternatization_zero_of_swap line 25

   Source documentation

   A symmetric pair of raw slots contributes zero to an exterior form.

   theorem raw_alternatization_zero_of_swap
       (a : MultilinearMap ℝ (fun _ : ι => E) ℂ) {i j : ι} (hij : i ≠ j)
       (h : a.domDomCongr (Equiv.swap i j) = a) : a.alternatization = 0 := by
   …