Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit e875492

Browse files
alexjbestmergify[bot]
authored andcommitted
chore(algebra/module) remove an unneeded commutativity assumption (#1813)
1 parent 5dae5d2 commit e875492

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/algebra/module.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@ begin
218218
end
219219

220220
--TODO: move
221-
lemma is_linear_map_smul' {α R : Type*} [add_comm_group α] [comm_ring R] [module R α] (a : α) :
221+
lemma is_linear_map_smul' {α R : Type*} [add_comm_group α] [ring R] [module R α] (a : α) :
222222
is_linear_map R (λ (c : R), c • a) :=
223223
begin
224224
refine is_linear_map.mk (λ x y, add_smul x y a) _,

0 commit comments

Comments
 (0)