Theorem 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 →