Def Algebra.Generators.naive

Modification history

2025-07-03 03:52

Mathlib/RingTheory/Extension/Generators.lean

feat(RingTheory/Presentation): naive presentations of quotients (#26650)

Added Algebra.Generators.naive View on Github →