Skip to content

[Merged by Bors] - chore(Topology/Algebra/Module/LinearMap): deprecate_module#39668

Closed
ADedecker wants to merge 3 commits into
leanprover-community:masterfrom
ADedecker:AD_deprecate_module_CLM
Closed

[Merged by Bors] - chore(Topology/Algebra/Module/LinearMap): deprecate_module#39668
ADedecker wants to merge 3 commits into
leanprover-community:masterfrom
ADedecker:AD_deprecate_module_CLM