Commit 2023-09-02 16:56 8953aea3

View on Github →

fix: remove a bad Algebra instance in FractionRing (#6724)

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem FractionRing.isScalarTower_liftAlgebra

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/WittVector/Isocrystal.lean