mathlib3

a1a0940c - chore(ring_theory/ideal): mark `ideal.quotient` as reducible (#7892)

chore(ring_theory/ideal): mark `ideal.quotient` as reducible (#7892) I had an ideal and wanted to apply a theorem about submodule quotients to the ideal quotient. The API around ideals is designed to have most things defeq to the corresponding submodule definition. Marking this definition as reducible informs the typeclass system that it can use this defeq. Test case: ````lean import ring_theory.ideal.basic /-- Typeclass instances on ideal quotients transfer to submodule quotients. This is useful if you want to apply results that hold for general submodules to ideals specifically. The instance will not be found if `ideal.quotient` is not reducible, e.g. after you uncomment the following line: ``` local attribute [semireducible] ideal.quotient ``` -/ example {R : Type*} [comm_ring R] (I : ideal R) [fintype (ideal.quotient I)] : fintype (submodule.quotient I) := infer_instance ```` Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Making.20.60ideal.2Equotient.60.20reducible.20.28or.20deleted.20altogether.3F.29