Commit 2023-06-15 22:49 c993cb10
View on Github →chore: use mathport output in FieldTheory.SplittingField.Construction (#5087) The mathlib3 version was manually backported from the mathlib4 version. We use here the mathport output.
chore: use mathport output in FieldTheory.SplittingField.Construction (#5087) The mathlib3 version was manually backported from the mathlib4 version. We use here the mathport output.