Mathlib v3 is deprecated. Go to Mathlib v4

Theorem power_basis.minpoly_gen_map

Modification history

2021-06-25 09:21

src/ring_theory/power_basis.lean

feat(ring_theory/power_basis): map a power basis through an alg_equiv (#8039) …

Added power_basis.minpoly_gen_map View on Github →