Skip to content

Commit

Permalink
style: fix wrapping of where (#7149)
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser authored and kodyvajjha committed Sep 22, 2023
1 parent e55ac24 commit 18cf985
Show file tree
Hide file tree
Showing 124 changed files with 463 additions and 451 deletions.
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Algebra/Equiv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -760,12 +760,12 @@ instance apply_faithfulSMul : FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁ :=
⟨AlgEquiv.ext⟩
#align alg_equiv.apply_has_faithful_smul AlgEquiv.apply_faithfulSMul

instance apply_smulCommClass : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁
where smul_comm r e a := (e.map_smul r a).symm
instance apply_smulCommClass : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁ where
smul_comm r e a := (e.map_smul r a).symm
#align alg_equiv.apply_smul_comm_class AlgEquiv.apply_smulCommClass

instance apply_smulCommClass' : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁
where smul_comm e r a := e.map_smul r a
instance apply_smulCommClass' : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁ where
smul_comm e r a := e.map_smul r a
#align alg_equiv.apply_smul_comm_class' AlgEquiv.apply_smulCommClass'

@[simp]
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -233,15 +233,15 @@ instance instIsScalarTower' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTow
IsScalarTower R' R S :=
S.toSubmodule.isScalarTower

instance [IsScalarTower R A A] : IsScalarTower R S S
where smul_assoc r x y := Subtype.ext <| smul_assoc r (x : A) (y : A)
instance [IsScalarTower R A A] : IsScalarTower R S S where
smul_assoc r x y := Subtype.ext <| smul_assoc r (x : A) (y : A)

instance instSMulCommClass' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A]
[SMulCommClass R' R A] : SMulCommClass R' R S
where smul_comm r' r s := Subtype.ext <| smul_comm r' r (s : A)
[SMulCommClass R' R A] : SMulCommClass R' R S where
smul_comm r' r s := Subtype.ext <| smul_comm r' r (s : A)

instance instSMulCommClass [SMulCommClass R A A] : SMulCommClass R S S
where smul_comm r x y := Subtype.ext <| smul_comm r (x : A) (y : A)
instance instSMulCommClass [SMulCommClass R A A] : SMulCommClass R S S where
smul_comm r x y := Subtype.ext <| smul_comm r (x : A) (y : A)

end

Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/GroupCat/Limits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -127,8 +127,8 @@ set_option linter.uppercaseLean3 false in

/-- The category of groups has all limits. -/
@[to_additive "The category of additive groups has all limits."]
instance hasLimitsOfSize : HasLimitsOfSize.{v, v} GroupCatMax.{v, u}
where has_limits_of_shape J _ :=
instance hasLimitsOfSize : HasLimitsOfSize.{v, v} GroupCatMax.{v, u} where
has_limits_of_shape J _ :=
{ has_limit :=
-- Porting note: add this instance to help Lean unify universe levels
fun F => letI : HasLimit (F ⋙ forget₂ GroupCatMax.{v, u} MonCat.{max v u}) :=
Expand Down Expand Up @@ -318,8 +318,8 @@ of groups.)
(That is, the underlying group could have been computed instead as limits in the category
of additive groups.)"]
noncomputable instance forget₂GroupPreservesLimitsOfSize :
PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCatMax.{v, u} GroupCatMax.{v, u})
where preservesLimitsOfShape {J 𝒥} := { preservesLimit := fun {F} => by infer_instance }
PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCatMax.{v, u} GroupCatMax.{v, u}) where
preservesLimitsOfShape {J 𝒥} := { preservesLimit := fun {F} => by infer_instance }
set_option linter.uppercaseLean3 false in
#align CommGroup.forget₂_Group_preserves_limits_of_size CommGroupCat.forget₂GroupPreservesLimitsOfSize
set_option linter.uppercaseLean3 false in
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ set_option linter.uppercaseLean3 false in
#align Module.forget₂_AddCommGroup_full ModuleCat.forget₂AddCommGroupFull

/-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
instance forget₂_addCommGroupCat_essSurj : EssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u})
where mem_essImage A :=
instance forget₂_addCommGroupCat_essSurj : EssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) where
mem_essImage A :=
⟨ModuleCat.of ℤ A,
⟨{ hom := 𝟙 A
inv := 𝟙 A }⟩⟩
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/GroupWithZeroCat.lean
Original file line number Diff line number Diff line change
Expand Up @@ -75,15 +75,15 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where

-- porting note: added
@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl
instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed
where forget₂ :=
instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where
forget₂ :=
{ obj := fun X => ⟨X, 0, 1
map := fun f => ⟨f, f.map_zero', f.map_one'⟩ }
set_option linter.uppercaseLean3 false in
#align GroupWithZero.has_forget_to_Bipointed GroupWithZeroCat.hasForgetToBipointed

instance hasForgetToMon : HasForget₂ GroupWithZeroCat MonCat
where forget₂ :=
instance hasForgetToMon : HasForget₂ GroupWithZeroCat MonCat where
forget₂ :=
{ obj := fun X => ⟨ X , _ ⟩
map := fun f => f.toMonoidHom }
set_option linter.uppercaseLean3 false in
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Category/MonCat/Colimits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -243,8 +243,8 @@ def colimitIsColimit : IsColimit (colimitCocone F) where
set_option linter.uppercaseLean3 false in
#align Mon.colimits.colimit_is_colimit MonCat.Colimits.colimitIsColimit

instance hasColimits_monCat : HasColimits MonCat
where has_colimits_of_shape _ _ :=
instance hasColimits_monCat : HasColimits MonCat where
has_colimits_of_shape _ _ :=
{ has_colimit := fun F =>
HasColimit.mk
{ cocone := colimitCocone F
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/Ring/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -121,8 +121,8 @@ instance hasForgetToMonCat : HasForget₂ SemiRingCat MonCat :=
set_option linter.uppercaseLean3 false in
#align SemiRing.has_forget_to_Mon SemiRingCat.hasForgetToMonCat

instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat
where -- can't use BundledHom.mkHasForget₂, since AddCommMon is an induced category
instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat where
-- can't use BundledHom.mkHasForget₂, since AddCommMon is an induced category
forget₂ :=
{ obj := fun R => AddCommMonCat.of R
-- Porting note: This doesn't work without the `(_ := _)` trick.
Expand Down Expand Up @@ -254,8 +254,8 @@ instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat :=
set_option linter.uppercaseLean3 false in
#align Ring.has_forget_to_SemiRing RingCat.hasForgetToSemiRingCat

instance hasForgetToAddCommGroupCat : HasForget₂ RingCat AddCommGroupCat
where -- can't use BundledHom.mkHasForget₂, since AddCommGroup is an induced category
instance hasForgetToAddCommGroupCat : HasForget₂ RingCat AddCommGroupCat where
-- can't use BundledHom.mkHasForget₂, since AddCommGroup is an induced category
forget₂ :=
{ obj := fun R => AddCommGroupCat.of R
-- Porting note: use `(_ := _)` similar to above.
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/DirectSum/Module.lean
Original file line number Diff line number Diff line change
Expand Up @@ -338,8 +338,8 @@ theorem IsInternal.submodule_independent (h : IsInternal A) : CompleteLattice.In
/-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
noncomputable def IsInternal.collectedBasis (h : IsInternal A) {α : ι → Type*}
(v : ∀ i, Basis (α i) R (A i)) : Basis (Σi, α i) R M
where repr :=
(v : ∀ i, Basis (α i) R (A i)) : Basis (Σi, α i) R M where
repr :=
((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ≪≫ₗ
DFinsupp.mapRange.linearEquiv fun i ↦ (v i).repr) ≪≫ₗ
(sigmaFinsuppLequivDFinsupp R).symm
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Algebra/GradedMonoid.lean
Original file line number Diff line number Diff line change
Expand Up @@ -263,8 +263,8 @@ variable [AddZeroClass ι] [GMul A]
/-- `(•) : A 0 → A i → A i` is the value provided in `GradedMonoid.GMul.mul`, composed with
an `Eq.rec` to turn `A (0 + i)` into `A i`.
-/
instance GradeZero.smul (i : ι) : SMul (A 0) (A i)
where smul x y := @Eq.rec ι (0+i) (fun a _ => A a) (GMul.mul x y) i (zero_add i)
instance GradeZero.smul (i : ι) : SMul (A 0) (A i) where
smul x y := @Eq.rec ι (0+i) (fun a _ => A a) (GMul.mul x y) i (zero_add i)
#align graded_monoid.grade_zero.has_smul GradedMonoid.GradeZero.smul

/-- `(*) : A 0 → A 0 → A 0` is the value provided in `GradedMonoid.GMul.mul`, composed with
Expand Down Expand Up @@ -496,8 +496,8 @@ theorem SetLike.one_mem_graded {S : Type*} [SetLike S R] [One R] [Zero ι] (A :
#align set_like.one_mem_graded SetLike.one_mem_graded

instance SetLike.gOne {S : Type*} [SetLike S R] [One R] [Zero ι] (A : ι → S)
[SetLike.GradedOne A] : GradedMonoid.GOne fun i => A i
where one := ⟨1, SetLike.one_mem_graded _⟩
[SetLike.GradedOne A] : GradedMonoid.GOne fun i => A i where
one := ⟨1, SetLike.one_mem_graded _⟩
#align set_like.ghas_one SetLike.gOne

@[simp]
Expand All @@ -518,8 +518,8 @@ theorem SetLike.mul_mem_graded {S : Type*} [SetLike S R] [Mul R] [Add ι] {A :
#align set_like.mul_mem_graded SetLike.mul_mem_graded

instance SetLike.gMul {S : Type*} [SetLike S R] [Mul R] [Add ι] (A : ι → S)
[SetLike.GradedMul A] : GradedMonoid.GMul fun i => A i
where mul := fun a b => ⟨(a * b : R), SetLike.mul_mem_graded a.prop b.prop⟩
[SetLike.GradedMul A] : GradedMonoid.GMul fun i => A i where
mul := fun a b => ⟨(a * b : R), SetLike.mul_mem_graded a.prop b.prop⟩
#align set_like.ghas_mul SetLike.gMul

/-
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/GradedMulAction.lean
Original file line number Diff line number Diff line change
Expand Up @@ -120,8 +120,8 @@ class SetLike.GradedSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M

instance SetLike.toGSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [Add ι]
(A : ι → S) (B : ι → N) [SetLike.GradedSmul A B] :
GradedMonoid.GSmul (fun i ↦ A i) fun i ↦ B i
where smul a b := ⟨a.1 • b.1, SetLike.GradedSmul.smul_mem a.2 b.2
GradedMonoid.GSmul (fun i ↦ A i) fun i ↦ B i where
smul a b := ⟨a.1 • b.1, SetLike.GradedSmul.smul_mem a.2 b.2
#align set_like.ghas_smul SetLike.toGSmul

/-
Expand All @@ -141,8 +141,8 @@ theorem SetLike.coe_GSmul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R

/-- Internally graded version of `Mul.toSMul`. -/
instance SetLike.GradedMul.toGradedSmul [AddMonoid ι] [Monoid R] {S : Type*} [SetLike S R]
(A : ι → S) [SetLike.GradedMonoid A] : SetLike.GradedSmul A A
where smul_mem _ _ _ _ hi hj := SetLike.GradedMonoid.toGradedMul.mul_mem hi hj
(A : ι → S) [SetLike.GradedMonoid A] : SetLike.GradedSmul A A where
smul_mem _ _ _ _ hi hj := SetLike.GradedMonoid.toGradedMul.mul_mem hi hj
#align set_like.has_graded_mul.to_has_graded_smul SetLike.GradedMul.toGradedSmul

end Subobjects
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/Additive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -199,8 +199,8 @@ between those functors applied to homological complexes.
-/
@[simps]
def NatTrans.mapHomologicalComplex {F G : V ⥤ W} [F.Additive] [G.Additive] (α : F ⟶ G)
(c : ComplexShape ι) : F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c
where app C := { f := fun i => α.app _ }
(c : ComplexShape ι) : F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c where
app C := { f := fun i => α.app _ }
#align category_theory.nat_trans.map_homological_complex CategoryTheory.NatTrans.mapHomologicalComplex

@[simp]
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/HomologicalComplex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -248,8 +248,8 @@ def id (A : HomologicalComplex V c) : Hom A A where f _ := 𝟙 _
#align homological_complex.id HomologicalComplex.id

/-- Composition of chain maps. -/
def comp (A B C : HomologicalComplex V c) (φ : Hom A B) (ψ : Hom B C) : Hom A C
where f i := φ.f i ≫ ψ.f i
def comp (A B C : HomologicalComplex V c) (φ : Hom A B) (ψ : Hom B C) : Hom A C where
f i := φ.f i ≫ ψ.f i
#align homological_complex.comp HomologicalComplex.comp

section
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Homology/LocalCohomology.lean
Original file line number Diff line number Diff line change
Expand Up @@ -159,8 +159,8 @@ def SelfLERadical (J : Ideal R) : Type u :=
instance (J : Ideal R) : Category (SelfLERadical J) :=
(FullSubcategory.category _)

instance SelfLERadical.inhabited (J : Ideal R) : Inhabited (SelfLERadical J)
where default := ⟨J, Ideal.le_radical⟩
instance SelfLERadical.inhabited (J : Ideal R) : Inhabited (SelfLERadical J) where
default := ⟨J, Ideal.le_radical⟩
#align local_cohomology.self_le_radical.inhabited localCohomology.SelfLERadical.inhabited

/-- The diagram of all ideals with radical containing `J`, represented as a functor.
Expand Down
16 changes: 8 additions & 8 deletions Mathlib/Algebra/Lie/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -866,11 +866,11 @@ def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse
}
#align lie_module_hom.inverse LieModuleHom.inverse

instance : Add (M →ₗ⁅R,L⁆ N)
where add f g := { (f : M →ₗ[R] N) + (g : M →ₗ[R] N) with map_lie' := by simp }
instance : Add (M →ₗ⁅R,L⁆ N) where
add f g := { (f : M →ₗ[R] N) + (g : M →ₗ[R] N) with map_lie' := by simp }

instance : Sub (M →ₗ⁅R,L⁆ N)
where sub f g := { (f : M →ₗ[R] N) - (g : M →ₗ[R] N) with map_lie' := by simp }
instance : Sub (M →ₗ⁅R,L⁆ N) where
sub f g := { (f : M →ₗ[R] N) - (g : M →ₗ[R] N) with map_lie' := by simp }

instance : Neg (M →ₗ⁅R,L⁆ N) where neg f := { -(f : M →ₗ[R] N) with map_lie' := by simp }

Expand Down Expand Up @@ -901,8 +901,8 @@ theorem neg_apply (f : M →ₗ⁅R,L⁆ N) (m : M) : (-f) m = -f m :=
rfl
#align lie_module_hom.neg_apply LieModuleHom.neg_apply

instance hasNsmul : SMul ℕ (M →ₗ⁅R,L⁆ N)
where smul n f := { n • (f : M →ₗ[R] N) with map_lie' := by simp }
instance hasNsmul : SMul ℕ (M →ₗ⁅R,L⁆ N) where
smul n f := { n • (f : M →ₗ[R] N) with map_lie' := by simp }
#align lie_module_hom.has_nsmul LieModuleHom.hasNsmul

@[norm_cast, simp]
Expand All @@ -914,8 +914,8 @@ theorem nsmul_apply (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (n • f) m =
rfl
#align lie_module_hom.nsmul_apply LieModuleHom.nsmul_apply

instance hasZsmul : SMul ℤ (M →ₗ⁅R,L⁆ N)
where smul z f := { z • (f : M →ₗ[R] N) with map_lie' := by simp }
instance hasZsmul : SMul ℤ (M →ₗ⁅R,L⁆ N) where
smul z f := { z • (f : M →ₗ[R] N) with map_lie' := by simp }
#align lie_module_hom.has_zsmul LieModuleHom.hasZsmul

@[norm_cast, simp]
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Lie/Free.lean
Original file line number Diff line number Diff line change
Expand Up @@ -126,18 +126,18 @@ instance {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] :
SMul S (FreeLieAlgebra R X) where smul t := Quot.map ((· • ·) t) (Rel.smulOfTower t)

instance {S : Type*} [Monoid S] [DistribMulAction S R] [DistribMulAction Sᵐᵒᵖ R]
[IsScalarTower S R R] [IsCentralScalar S R] : IsCentralScalar S (FreeLieAlgebra R X)
where op_smul_eq_smul t := Quot.ind fun a => congr_arg (Quot.mk _) (op_smul_eq_smul t a)
[IsScalarTower S R R] [IsCentralScalar S R] : IsCentralScalar S (FreeLieAlgebra R X) where
op_smul_eq_smul t := Quot.ind fun a => congr_arg (Quot.mk _) (op_smul_eq_smul t a)

instance : Zero (FreeLieAlgebra R X) where zero := Quot.mk _ 0

instance : Add (FreeLieAlgebra R X)
where add := Quot.map₂ (· + ·) (fun _ _ _ => Rel.addLeft _) fun _ _ _ => Rel.add_right _
instance : Add (FreeLieAlgebra R X) where
add := Quot.map₂ (· + ·) (fun _ _ _ => Rel.addLeft _) fun _ _ _ => Rel.add_right _

instance : Neg (FreeLieAlgebra R X) where neg := Quot.map Neg.neg fun _ _ => Rel.neg

instance : Sub (FreeLieAlgebra R X)
where sub := Quot.map₂ Sub.sub (fun _ _ _ => Rel.subLeft _) fun _ _ _ => Rel.subRight _
instance : Sub (FreeLieAlgebra R X) where
sub := Quot.map₂ Sub.sub (fun _ _ _ => Rel.subLeft _) fun _ _ _ => Rel.subRight _

instance : AddGroup (FreeLieAlgebra R X) :=
Function.Surjective.addGroup (Quot.mk _) (surjective_quot_mk _) rfl (fun _ _ => rfl)
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Lie/Subalgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -116,8 +116,8 @@ instance (L' : LieSubalgebra R L) [IsNoetherian R L] : IsNoetherian R L' :=
end

/-- A Lie subalgebra forms a new Lie algebra. -/
instance lieAlgebra (L' : LieSubalgebra R L) : LieAlgebra R L'
where lie_smul := by
instance lieAlgebra (L' : LieSubalgebra R L) : LieAlgebra R L' where
lie_smul := by
{ intros
apply SetCoe.ext
apply lie_smul }
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Module/Equiv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -692,12 +692,12 @@ instance apply_faithfulSMul : FaithfulSMul (M ≃ₗ[R] M) M :=
⟨@fun _ _ => LinearEquiv.ext⟩
#align linear_equiv.apply_has_faithful_smul LinearEquiv.apply_faithfulSMul

instance apply_smulCommClass : SMulCommClass R (M ≃ₗ[R] M) M
where smul_comm r e m := (e.map_smul r m).symm
instance apply_smulCommClass : SMulCommClass R (M ≃ₗ[R] M) M where
smul_comm r e m := (e.map_smul r m).symm
#align linear_equiv.apply_smul_comm_class LinearEquiv.apply_smulCommClass

instance apply_smulCommClass' : SMulCommClass (M ≃ₗ[R] M) R M
where smul_comm := LinearEquiv.map_smul
instance apply_smulCommClass' : SMulCommClass (M ≃ₗ[R] M) R M where
smul_comm := LinearEquiv.map_smul
#align linear_equiv.apply_smul_comm_class' LinearEquiv.apply_smulCommClass'

end Automorphisms
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Module/GradedModule.lean
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ section

open GradedMonoid DirectSum Gmodule

instance [DecidableEq ι] [GMonoid A] [Gmodule A M] : SMul (⨁ i, A i) (⨁ i, M i)
where smul x y := smulAddMonoidHom A M x y
instance [DecidableEq ι] [GMonoid A] [Gmodule A M] : SMul (⨁ i, A i) (⨁ i, M i) where
smul x y := smulAddMonoidHom A M x y

@[simp]
theorem smul_def [DecidableEq ι] [GMonoid A] [Gmodule A M] (x : ⨁ i, A i) (y : ⨁ i, M i) :
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Module/LinearMap.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1159,12 +1159,12 @@ instance apply_faithfulSMul : FaithfulSMul (Module.End R M) M :=
⟨LinearMap.ext⟩
#align linear_map.apply_has_faithful_smul LinearMap.apply_faithfulSMul

instance apply_smulCommClass : SMulCommClass R (Module.End R M) M
where smul_comm r e m := (e.map_smul r m).symm
instance apply_smulCommClass : SMulCommClass R (Module.End R M) M where
smul_comm r e m := (e.map_smul r m).symm
#align linear_map.apply_smul_comm_class LinearMap.apply_smulCommClass

instance apply_smulCommClass' : SMulCommClass (Module.End R M) R M
where smul_comm := LinearMap.map_smul
instance apply_smulCommClass' : SMulCommClass (Module.End R M) R M where
smul_comm := LinearMap.map_smul
#align linear_map.apply_smul_comm_class' LinearMap.apply_smulCommClass'

instance apply_isScalarTower {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Module/Submodule/Pointwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,8 @@ Recall that When `R` is the semiring corresponding to the nonnegative elements o
`Submodule R' M` is the type of cones of `M`. This instance reflects such cones about `0`.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseNeg : Neg (Submodule R M)
where neg p :=
protected def pointwiseNeg : Neg (Submodule R M) where
neg p :=
{ -p.toAddSubmonoid with
carrier := -(p : Set M)
smul_mem' := fun r m hm => Set.mem_neg.2 <| smul_neg r m ▸ p.smul_mem r <| Set.mem_neg.1 hm }
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Order/Nonneg/Ring.lean
Original file line number Diff line number Diff line change
Expand Up @@ -199,8 +199,8 @@ theorem mk_eq_one [OrderedSemiring α] {x : α} (hx : 0 ≤ x) :
Subtype.ext_iff
#align nonneg.mk_eq_one Nonneg.mk_eq_one

instance mul [OrderedSemiring α] : Mul { x : α // 0 ≤ x }
where mul x y := ⟨x * y, mul_nonneg x.2 y.2
instance mul [OrderedSemiring α] : Mul { x : α // 0 ≤ x } where
mul x y := ⟨x * y, mul_nonneg x.2 y.2
#align nonneg.has_mul Nonneg.mul

@[simp, norm_cast]
Expand Down Expand Up @@ -233,8 +233,8 @@ theorem mk_nat_cast [OrderedSemiring α] (n : ℕ) : (⟨n, n.cast_nonneg⟩ : {
rfl
#align nonneg.mk_nat_cast Nonneg.mk_nat_cast

instance pow [OrderedSemiring α] : Pow { x : α // 0 ≤ x } ℕ
where pow x n := ⟨(x : α) ^ n, pow_nonneg x.2 n⟩
instance pow [OrderedSemiring α] : Pow { x : α // 0 ≤ x } ℕ where
pow x n := ⟨(x : α) ^ n, pow_nonneg x.2 n⟩
#align nonneg.has_pow Nonneg.pow

@[simp, norm_cast]
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Quaternion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -353,11 +353,11 @@ variable [SMul S R] [SMul T R] (s : S)
-- porting note: Lean 4 auto drops the unused `[Ring R]` argument
instance : SMul S ℍ[R,c₁,c₂] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4

instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂]
where smul_assoc s t x := by ext <;> exact smul_assoc _ _ _
instance [SMul S T] [IsScalarTower S T R] : IsScalarTower S T ℍ[R,c₁,c₂] where
smul_assoc s t x := by ext <;> exact smul_assoc _ _ _

instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂]
where smul_comm s t x := by ext <;> exact smul_comm _ _ _
instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂] where
smul_comm s t x := by ext <;> exact smul_comm _ _ _

@[simp] theorem smul_re : (s • a).re = s • a.re := rfl
#align quaternion_algebra.smul_re QuaternionAlgebra.smul_re
Expand Down
Loading

0 comments on commit 18cf985

Please sign in to comment.