Theorems · Theorem · ring theory

Set.neg_smul_set

∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] (a : α) (t : Set β),
  -a • t = -(a • t)

Defined in

Mathlib.Algebra.Ring.Action.Pointwise.Set

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModule