This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(ring_theory/graded_algebra): use `add_submonoid_class` to generalize to graded rings #14583

Closed

eric-wieser wants to merge 25 commits into master from eric-wieser/graded_ring

Closed

[Merged by Bors] - refactor(ring_theory/graded_algebra): use `add_submonoid_class` to generalize to graded rings #14583

rebuild please

Workflow runs completed with no jobs