Theorems · Theorem · group theory

Set.op_vadd_set_vadd_eq_vadd_vadd_set

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd αᵃᵒᵖ β] [inst_1 : VAdd β γ] [inst_2 : VAdd α γ] (a : α)
  (s : Set β) (t : Set γ),
  (∀ (a : α) (b : β) (c : γ), (AddOpposite.op a +ᵥ b) +ᵥ c = b +ᵥ a +ᵥ c) → (AddOpposite.op a +ᵥ s) +ᵥ t = s +ᵥ a +ᵥ t

Defined in

Mathlib.Algebra.Group.Pointwise.Set.Scalar

Cited by

1 results in Mathlib

Foundations

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

Assumes

VAddVAddVAdd