Add "ready-to-merge" and "delegated" label

[Merged by Bors] - feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions #29938

Sign in to view logs

Triggered via issue February 13, 2025 06:22

mathlib-bors[bot]

commented on #20899 e2c6f0e

Status Success

Total duration 11s

Artifacts –

maintainer_bors.yml

on: issue_comment

Add ready-to-merge or delegated label