Commit 2023-09-18 04:21 b955f55b

View on Github →

chore: replace minpoly.eq_of_algebraMap_eq by algebraMap_eq (#7228) Also changes the repetitive names minpoly.minpoly_algHom/Equiv to minpoly.algHom/Equiv_eq

Estimated changes

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Adjoin.lean

modified theorem IntermediateField.minpoly_gen

Modified Mathlib/FieldTheory/IntermediateField.lean

modified theorem IntermediateField.minpoly_eq

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

added theorem minpoly.algEquiv_eq

added theorem minpoly.algHom_eq

added theorem minpoly.algebraMap_eq

deleted theorem minpoly.minpoly_algEquiv

deleted theorem minpoly.minpoly_algHom

Modified Mathlib/FieldTheory/Minpoly/Field.lean

deleted theorem minpoly.eq_of_algebraMap_eq

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/FieldTheory/NormalClosure.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/Trace.lean