restrictScalars_neg — Mathlib

English

The negation restriction lemma states the same as above under the appropriate parameters.

Русский

Лемма ограниченийNeg говорит то же самое при соответствующих параметрах.

LaTeX

$$restrictScalars_neg {M N : Type*} [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R$$

Lean4

@[simp]
theorem restrictScalars_neg {M N : Type*} [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [Module S M]
    [Module S N] [CompatibleSMul M N R S] (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R :=
  rfl

Похожие утверждения