Skip to content

[Merged by Bors] - feat(RingTheory/MvPowerSeries/NoZeroDivisors): simplify the proof by adding exists_wellFoundedGT#36892

Closed
AntoineChambert-Loir wants to merge 10 commits intoleanprover-community:masterfrom
AntoineChambert-Loir:ACL-EWInstances
Closed

[Merged by Bors] - feat(RingTheory/MvPowerSeries/NoZeroDivisors): simplify the proof by adding exists_wellFoundedGT#36892
AntoineChambert-Loir wants to merge 10 commits intoleanprover-community:masterfrom
AntoineChambert-Loir:ACL-EWInstances

Commits