<div id="comment:0"></div> but there remains some uses in the same file Part of #26902. Follow-up ticket: #34771 CC: @tscrim @slel @kwankyu @kliem Component: **coding theory** Author: **Frédéric Chapoton** Branch: **[`d86dd0c`](https://github.com/sagemath/sagetrac-mirror/commit/d86dd0c79ca6b59dbfae69960fac3a60d0bc8485)** Reviewer: **Kwankyu Lee** _Issue created by migration from https://trac.sagemath.org/ticket/34737_