Theorem Algebra.Presentation.naive_relation

Modification history

2026-04-23 11:33
Mathlib/RingTheory/Extension/Presentation/Basic.lean
chore(RingTheory/Extension): remove `backward.privateInPublic` (#38389)
Modified Algebra.Presentation.naive_relationView on Github →
2025-07-03 03:52
Mathlib/RingTheory/Extension/Presentation/Basic.lean
feat(RingTheory/Presentation): naive presentations of quotients (#26650)
Added Algebra.Presentation.naive_relationView on Github →