Replace `AlgNb` by `IntgRing` from @digama0 's mathbox (#4632) · metamath/set.mm@c800cbc · GitHub

Commit

Replace AlgNb by IntgRing from @digama0 's mathbox (#4632)

Browse files

* Replace `AlgNb` by `IntgRing` from @digama0 's mathbox

* Fix comment and definitional soundness check

* As per @icecream17 's comments

* As per @avekens  's comments

Loading branch information

tirix authored Feb 8, 2025

1 parent 1f1ab7c commit c800cbc