Commit 2023-06-23 12:17 ec5e5e75

View on Github →

chore: use _root_. as in mathlib3 (#5420) These are the mathlib3 names.

Estimated changes

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

added def Algebra.adjoin.powerBasis'

deleted def minpoly.Algebra.adjoin.powerBasis'

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean