English
A variant of associativity for nested kroneckerMap with a weaker structural equality h.
Русский
Упрощённая формулировка ассоциативности для вложенного kroneckerMap с меньшей структурной точностью h.
LaTeX
$$$\text{reindex} (\mathrm{prodAssoc}\ l n q) (\mathrm{prodAssoc}\ m p r) (\operatorname{kroneckerMap} g (\operatorname{kroneckerMap} f A B) D) = \operatorname{kroneckerMap} f' A (\operatorname{kroneckerMap} g' B D)$$$
Lean4
theorem kroneckerMap_assoc₁ {δ ξ ω : Type*} (f : α → β → γ) (g : γ → δ → ω) (f' : α → ξ → ω) (g' : β → δ → ξ)
(A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ) (h : ∀ a b d, g (f a b) d = f' a (g' b d)) :
reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (kroneckerMap g (kroneckerMap f A B) D) =
kroneckerMap f' A (kroneckerMap g' B D) :=
ext fun _ _ => h _ _ _
