Def Module.Relations.Solution.fromQuotient

Modification history

2026-03-28 11:48
Mathlib/Algebra/Module/Presentation/Basic.lean
chore: avoid `dsimp; infer_instance` (#37288) …
Added Module.Relations.Solution.fromQuotientView on Github →