Theorems · Definition · group theory

SubAddAction.ofFixingAddSubgroup_of_eq

(M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} →
          (hst : s = t) →
            have φ := AddEquiv.addSubgroupCongr ⋯;
            ↥(SubAddAction.ofFixingAddSubgroup M s) →ₑ[⇑φ] ↥(SubAddAction.ofFixingAddSubgroup M t)

The identity between the SubAddActions of fixingAddSubgroups of equal sets, as an equivariant map.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction