Def Module.Relations.Solution.IsPresentation.uniq

Modification history

2026-08-03 21:26

Mathlib/Algebra/Module/Presentation/Basic.lean

refactor(Algebra/Module/Equiv): update name and refactor API ofLinearEquiv (#40865) …

Modified Module.Relations.Solution.IsPresentation.uniq View on Github →

2026-03-28 11:48

Mathlib/Algebra/Module/Presentation/Basic.lean

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

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