Def Module.Relations.Solution.IsPresentation.linearEquiv

Modification history

2026-03-28 11:48

Mathlib/Algebra/Module/Presentation/Basic.lean

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

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