Commit 2024-10-29 15:17 f4f0b47a
View on Github →chore(RingTheory/Congruence): split off Defs.lean
(#18387)
The goal of this PR is to split off enough to define the ideal quotient and its ring structure without too much theory in the way.
chore(RingTheory/Congruence): split off Defs.lean
(#18387)
The goal of this PR is to split off enough to define the ideal quotient and its ring structure without too much theory in the way.