Theorem Algebra.adjoin.powerBasis'_gen

Modification history

2023-06-24 05:35
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
chore: don't use `simps` (#5423) …
Added Algebra.adjoin.powerBasis'_genView on Github →