Commit 2025-01-04 18:31 a36b4f2f
View on Github →chore(RingTheory/Generators): make algebra instance a def (#14265)
Makes the algebra instance Algebra P.Ring S
for P : Generators R S
a def and adds the instance attribute locally where needed. This prevents an instance diamond in the case where S
is a quotient of some polynomial algebra.
See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Diamond.20in.20.60Algebra.2EGenerators.60.