4.21. Tactic.KernelHom.Tactic.Reassoc🔗

kernel_reassoc

This file extends Mathlib.Tactic.CategoryTheory.Reassoc with a kernel-specific variant for equalities of s-finite kernels. It mirrors the structure of Mathlib.Tactic.CategoryTheory. Reassoc, but targets the kernel language developed in KernelHom rather than categorical morphisms.

Module LeanMachineLearning.Tactic.KernelHom.Tactic.Reassoc contains 6 exposed declarations.