Commit 2023-05-19 15:02 65012b46

View on Github →

feat: port RingTheory.FinitePresentation (#3316)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FinitePresentation.lean

added theorem AlgHom.FinitePresentation.comp

added theorem AlgHom.FinitePresentation.comp_surjective

added theorem AlgHom.FinitePresentation.id

added theorem AlgHom.FinitePresentation.of_finiteType

added theorem AlgHom.FinitePresentation.of_surjective

added def AlgHom.FinitePresentation

added theorem AlgHom.FiniteType.of_finitePresentation

added theorem Algebra.FinitePresentation.equiv

added theorem Algebra.FinitePresentation.iff

added theorem Algebra.FinitePresentation.iff_quotient_mvPolynomial'

added theorem Algebra.FinitePresentation.ker_fG_of_surjective

added theorem Algebra.FinitePresentation.ker_fg_of_mvPolynomial

added theorem Algebra.FinitePresentation.mvPolynomial_of_finitePresentation

added theorem Algebra.FinitePresentation.of_finiteType

added theorem Algebra.FinitePresentation.of_restrict_scalars_finitePresentation

added theorem Algebra.FinitePresentation.of_surjective

added theorem Algebra.FinitePresentation.polynomial

added theorem Algebra.FinitePresentation.self

added theorem Algebra.FinitePresentation.trans

added def Algebra.FinitePresentation

added theorem Algebra.FiniteType.of_finitePresentation

added theorem RingHom.FinitePresentation.comp

added theorem RingHom.FinitePresentation.comp_surjective

added theorem RingHom.FinitePresentation.id

added theorem RingHom.FinitePresentation.of_comp_finiteType

added theorem RingHom.FinitePresentation.of_finiteType

added theorem RingHom.FinitePresentation.of_surjective

added def RingHom.FinitePresentation

added theorem RingHom.FiniteType.of_finitePresentation