Theorem PowerBasis.ofAdjoinEqTop'_dim

Modification history

2025-09-29 15:37
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
feat(PowerBasis): various ways to create power bases (#29674) …
Added PowerBasis.ofAdjoinEqTop'_dimView on Github →