Repository navigation

Core: consolidate onto Mathlib's Splits API and general interlacing lemmas - #1996

Merged

PerAlexandersson merged 7 commits into

mainfrom

core/consolidate-1

Oct 21, 2026

Merged

Core: consolidate onto Mathlib's Splits API and general interlacing lemmas#1996
PerAlexandersson merged 7 commits into
mainfrom
core/consolidate-1

Commits on Oct 21, 2026
- Consolidate core onto Mathlib's Splits API and general lemmas
  
  PerAlexandersson
  and
  claude
  committed
  6dda5d3
- Merge remote-tracking branch 'origin/main' into core/consolidate-1
  PerAlexandersson
  committed
  c2a240a
- Drop unneeded nonnegativity hypotheses from common-factor interlacing
  
  PerAlexandersson
  and
  claude
  committed
  73a4b8b
- Document compatibility tactic forms; regenerate OEIS tactic coverage
  
  PerAlexandersson
  and
  claude
  committed
  1fbc53e
- Wrap compatibility tactic docstrings
  
  PerAlexandersson
  and
  claude
  committed
  c1ddba6
- Mark compatibility tactic forms as tactic_alt
  
  PerAlexandersson
  and
  claude
  committed
  18350dc
- Name compatibility tactic syntaxes in lowerCamelCase
  
  PerAlexandersson
  and
  claude
  committed
  7a178a5