Commit 2024-07-17 18:39 510d207f
View on Github →feat(Algebra/Module/LinearMap/Defs): add restrictScalars as a LinearMap (#14831)
add some missing lemmas on RestrictScalars as a Linear Map.
This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in
June 2024.