Theorem PowerBasis.ofGenMemAdjoin'_gen

Modification history

2025-09-29 15:37
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
feat(PowerBasis): various ways to create power bases (#29674) …
Deleted PowerBasis.ofGenMemAdjoin'_genView on Github →
2023-06-24 05:35
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
chore: don't use `simps` (#5423) …
Added PowerBasis.ofGenMemAdjoin'_genView on Github →