Theorems · Theorem · group theory
AddActionHom.map_mem_fixedBy
∀ {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddMonoid G] [inst_1 : AddAction G A] [inst_2 : AddAction G B]
(f : A →ₑ[id] B) {g : G} {a : A}, a ∈ AddAction.fixedBy A g → f a ∈ AddAction.fixedBy B gAddActionHom maps fixedBy to fixedBy.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- AddMonoidstatement and proof · cited by 2,864
- AddActionstatement and proof · cited by 820
- AddActionHomstatement and proof · cited by 82
- AddAction.fixedBystatement and proof · cited by 26
- AddAction.mem_fixedByproof · cited by 12
- map_vaddproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.