From 641f7a785069b207155dea875f0ab858853936d7 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 23 Jul 2023 09:39:59 +0000 Subject: [PATCH] fix: CompatibleSMul : Prop (#6065) Lean makes it `Type` otherwise. Why does this happen? Am I missing something? --- Mathlib/Algebra/Module/LinearMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index d24e3265ea7f5..b160ecc307635 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -399,7 +399,7 @@ we can also add an instance for `AddCommGroup.intModule`, allowing `z •` to be `R` does not support negation. -/ class CompatibleSMul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] - [Module S M₂] where + [Module S M₂] : Prop where /-- Scalar multiplication by `R` of `M` can be moved through linear maps. -/ map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x #align linear_map.compatible_smul LinearMap.CompatibleSMul