Theorems · Theorem · group theory

AddAction.Supports.vadd

∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup H] [inst_1 : VAdd G α]
  [inst_2 : VAdd G β] [inst_3 : AddAction H α] [inst_4 : VAdd H β] [VAddCommClass G H β] [VAddCommClass G H α]
  {s : Set α} {b : β} (g : H), AddAction.Supports G s b → AddAction.Supports G (g +ᵥ s) (g +ᵥ b)

Defined in: Mathlib.GroupTheory.GroupAction.Support
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Quot.sound
Assumes: AddGroup VAdd VAdd AddAction VAdd VAddCommClass VAddCommClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
AddGroupstatement and proof · cited by 4,410
HVAdd.hVAddstatement and proof · cited by 1,820
AddActionstatement and proof · cited by 820
VAddstatement and proof · cited by 616
Set.vaddSetstatement · cited by 403
Set.forall_mem_imageproof · cited by 65
VAddCommClassstatement and proof · cited by 41
VAddCommClass.vadd_commproof · cited by 19
vadd_left_cancel_iffproof · cited by 7
AddAction.Supportsstatement and proof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.