search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Prove that the ideal generated by a two-element set consists of linear combinations of those elements #43

Closed valis closed 2 years ago

valis commented 2 years ago

This is Algebra.Ring.Ideal/Ideal.closure2-lem. This can be generalized to any finite set of elements.

TurtlePU commented 2 years ago

I'll do it! Will PR in a while.