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.

Estimated changes