Commit 2024-04-14 18:26 22092a2a

View on Github →

chore(RingTheory/FinitePresentation): make Algebra.FinitePresentation a class (#12057) Makes Algebra.FinitePresentation a class, matching Algebra.FiniteType. Changes theorems to instances where possible.

Estimated changes

Modified Mathlib/RingTheory/FinitePresentation.lean

modified theorem Algebra.FinitePresentation.equiv

modified theorem Algebra.FinitePresentation.mvPolynomial_of_finitePresentation

deleted theorem Algebra.FinitePresentation.polynomial

deleted theorem Algebra.FinitePresentation.self

modified theorem Algebra.FinitePresentation.trans

deleted def Algebra.FinitePresentation

deleted theorem Algebra.FiniteType.of_finitePresentation