Theorem Algebra.FinitePresentation.mvPolynomial_of_finitePresentation

Modification history

2025-09-01 12:03
Mathlib/RingTheory/FinitePresentation.lean
chore(RingTheory): process porting notes, part 1 (#29112) …
Modified Algebra.FinitePresentation.mvPolynomial_of_finitePresentationView on Github →
2024-04-14 18:26
Mathlib/RingTheory/FinitePresentation.lean
chore(RingTheory/FinitePresentation): make `Algebra.FinitePresentation` a class (#12057) …
Modified Algebra.FinitePresentation.mvPolynomial_of_finitePresentationView on Github →
2023-05-19 15:02
Mathlib/RingTheory/FinitePresentation.lean
feat: port RingTheory.FinitePresentation (#3316)
Added Algebra.FinitePresentation.mvPolynomial_of_finitePresentationView on Github →