Def Module.Relations.Solution.IsPresentation.linearMapEquiv

Modification history

2026-03-28 11:48

Mathlib/Algebra/Module/Presentation/Basic.lean

chore: avoid `dsimp; infer_instance` (#37288) …

Added Module.Relations.Solution.IsPresentation.linearMapEquiv View on Github →