Theorems · Theorem · group theory
SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_addConj
∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α) (g : M),
fixingAddSubgroup M (g +ᵥ s) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.addConj g)) (fixingAddSubgroup M s)The fixingAddSubgroup of g +ᵥ s is the conjugate
of the fixingAddSubgroup of s by g.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement and proof · cited by 53,352
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- AddMonoidHomstatement · cited by 3,230
- HVAdd.hVAddstatement · cited by 1,820
- AddActionstatement and proof · cited by 820
- Set.vaddSetstatement · cited by 403
- AddSubgroup.mapstatement · cited by 189
- AddEquiv.toAddMonoidHomstatement · cited by 101
- AddAutstatement · cited by 75
- fixingAddSubgroupstatement · cited by 50
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.