Repository navigation

Add the `kernel_hom` tactic - #217

Merged

RemyDegenne merged 4 commits into

LeanMachineLearning:mainfrom

gaetanserre:kernelHom

Aug 21, 2026

Merged

Add the `kernel_hom` tactic#217
RemyDegenne merged 4 commits into
LeanMachineLearning:mainfrom
gaetanserre:kernelHom

Commits on Aug 20, 2026
- Add the `kernel_hom` tactic
  gaetanserre
  committed
  531ef96
- `simp` -> `rfl`
  gaetanserre
  committed
  2a6719a
- `kernel_lift` -> `kernel_hom`
  gaetanserre
  committed
  1411e72
- Remove useless measurable equivalences
  gaetanserre
  committed
  f2e6978