Commit 2023-04-04 12:51 544bdac2

View on Github →

feat: port RingTheory.ReesAlgebra (#3252)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/ReesAlgebra.lean

added theorem adjoin_monomial_eq_reesAlgebra

added theorem mem_reesAlgebra_iff

added theorem mem_reesAlgebra_iff_support

added theorem monomial_mem_adjoin_monomial

added theorem reesAlgebra.fg

added theorem reesAlgebra.monomial_mem

added def reesAlgebra