Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction

Sets invariant to a MulAction #

In this file we define SubMulAction R M; a subset of a MulAction R M which is closed with respect to scalar multiplication.

For most uses, typically Submodule R M is more powerful.

Main definitions #

Tags #

submodule, mul_action

class SMulMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [SMul R M] [SetLike S M] :

SMulMemClass S R M says S is a type of subsets s ≤ M that are closed under the scalar action of R on M.

Note that only R is marked as an outParam here, since M is supplied by the SetLike class instead.

  • smul_mem {s : S} (r : R) {m : M} : m sr m s

    Multiplication by a scalar on an element of the set remains in the set.

Instances
    class VAddMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [VAdd R M] [SetLike S M] :

    VAddMemClass S R M says S is a type of subsets s ≤ M that are closed under the additive action of R on M.

    Note that only R is marked as an outParam here, since M is supplied by the SetLike class instead.

    • vadd_mem {s : S} (r : R) {m : M} : m sr +ᵥ m s

      Addition by a scalar with an element of the set remains in the set.

    Instances

      Not registered as an instance because R is an outParam in SMulMemClass S R M.

      Not registered as an instance because R is an outParam in SMulMemClass S R M.

      @[instance 50]
      instance SetLike.smul {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) :
      SMul R s

      A subset closed under the scalar action inherits that action.

      Equations
        @[instance 50]
        instance SetLike.vadd {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) :
        VAdd R s

        A subset closed under the additive action inherits that action.

        Equations
          theorem SMulMemClass.ofIsScalarTower (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] :

          This can't be an instance because Lean wouldn't know how to find N, but we can still use this to manually derive SMulMemClass on specific types.

          theorem VAddMemClass.ofVAddAssocClass (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] :
          instance SetLike.instIsScalarTower {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] [Mul M] [MulMemClass S M] [IsScalarTower R M M] (s : S) :
          IsScalarTower R s s
          instance SetLike.instSMulCommClass {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] [Mul M] [MulMemClass S M] [SMulCommClass R M M] (s : S) :
          SMulCommClass R s s
          @[simp]
          theorem SetLike.val_smul {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : s) :
          ↑(r x) = r x
          @[simp]
          theorem SetLike.val_vadd {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : s) :
          ↑(r +ᵥ x) = r +ᵥ x
          @[simp]
          theorem SetLike.mk_smul_mk {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
          r x, hx = r x,
          @[simp]
          theorem SetLike.mk_vadd_mk {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
          r +ᵥ x, hx = r +ᵥ x,
          theorem SetLike.smul_def {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : s) :
          r x = r x,
          theorem SetLike.vadd_def {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : s) :
          r +ᵥ x = r +ᵥ x,
          @[simp]
          theorem SetLike.forall_smul_mem_iff {R : Type u_1} {M : Type u_2} {S : Type u_3} [Monoid R] [MulAction R M] [SetLike S M] [SMulMemClass S R M] {N : S} {x : M} :
          (∀ (a : R), a x N) x N
          @[instance 50]
          instance SetLike.smul' {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) :
          SMul M s

          A subset closed under the scalar action inherits that action.

          Equations
            @[instance 50]
            instance SetLike.vadd' {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) :
            VAdd M s

            A subset closed under the additive action inherits that action.

            Equations
              @[instance 50]
              instance SetLike.instIsScalarTowerSubtypeMem {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) :
              IsScalarTower M N s
              @[simp]
              theorem SetLike.val_smul_of_tower {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : s) :
              ↑(r x) = r x
              @[simp]
              theorem SetLike.val_vadd_of_tower {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : s) :
              ↑(r +ᵥ x) = r +ᵥ x
              @[simp]
              theorem SetLike.mk_smul_of_tower_mk {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : α) (hx : x s) :
              r x, hx = r x,
              @[simp]
              theorem SetLike.mk_vadd_of_tower_mk {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : α) (hx : x s) :
              r +ᵥ x, hx = r +ᵥ x,
              theorem SetLike.smul_of_tower_def {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : s) :
              r x = r x,
              theorem SetLike.vadd_of_tower_def {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : s) :
              r +ᵥ x = r +ᵥ x,
              structure SubAddAction (R : Type u) (M : Type v) [VAdd R M] :

              A SubAddAction is a set which is closed under scalar multiplication.

              Instances For
                structure SubMulAction (R : Type u) (M : Type v) [SMul R M] :

                A SubMulAction is a set which is closed under scalar multiplication.

                Instances For
                  instance SubMulAction.instSetLike {R : Type u} {M : Type v} [SMul R M] :
                  Equations
                    instance SubAddAction.instSetLike {R : Type u} {M : Type v} [VAdd R M] :
                    Equations
                      @[simp]
                      theorem SubMulAction.mem_carrier {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} {x : M} :
                      x p.carrier x p
                      @[simp]
                      theorem SubAddAction.mem_carrier {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} {x : M} :
                      x p.carrier x p
                      theorem SubMulAction.ext {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} (h : ∀ (x : M), x p x q) :
                      p = q
                      theorem SubAddAction.ext {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} (h : ∀ (x : M), x p x q) :
                      p = q
                      theorem SubMulAction.ext_iff {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} :
                      p = q ∀ (x : M), x p x q
                      theorem SubAddAction.ext_iff {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} :
                      p = q ∀ (x : M), x p x q
                      def SubMulAction.copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = p) :

                      Copy of a sub_mul_action with a new carrier equal to the old one. Useful to fix definitional equalities.

                      Equations
                        Instances For
                          def SubAddAction.copy {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = p) :

                          Copy of a sub_mul_action with a new carrier equal to the old one. Useful to fix definitional equalities.

                          Equations
                            Instances For
                              @[simp]
                              theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = p) :
                              (p.copy s hs) = s
                              @[simp]
                              theorem SubAddAction.coe_copy {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = p) :
                              (p.copy s hs) = s
                              theorem SubMulAction.copy_eq {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = p) :
                              p.copy s hs = p
                              theorem SubAddAction.copy_eq {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = p) :
                              p.copy s hs = p
                              instance SubMulAction.instBot {R : Type u} {M : Type v} [SMul R M] :
                              Equations
                                instance SubAddAction.instBot {R : Type u} {M : Type v} [VAdd R M] :
                                Equations
                                  instance SubMulAction.instInhabited {R : Type u} {M : Type v} [SMul R M] :
                                  Equations
                                    instance SubAddAction.instInhabited {R : Type u} {M : Type v} [VAdd R M] :
                                    Equations
                                      theorem SubMulAction.smul_mem {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) {x : M} (r : R) (h : x p) :
                                      r x p
                                      theorem SubAddAction.vadd_mem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) {x : M} (r : R) (h : x p) :
                                      r +ᵥ x p
                                      instance SubMulAction.instSMulSubtypeMem {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
                                      SMul R p
                                      Equations
                                        instance SubAddAction.instVAddSubtypeMem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) :
                                        VAdd R p
                                        Equations
                                          @[simp]
                                          theorem SubMulAction.val_smul {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} (r : R) (x : p) :
                                          ↑(r x) = r x
                                          @[simp]
                                          theorem SubAddAction.val_vadd {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} (r : R) (x : p) :
                                          ↑(r +ᵥ x) = r +ᵥ x
                                          def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
                                          p →ₑ[id] M

                                          Embedding of a submodule p to the ambient space M.

                                          Equations
                                            Instances For
                                              def SubAddAction.subtype {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) :
                                              p →ₑ[id] M

                                              Embedding of a submodule p to the ambient space M.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} (x : p) :
                                                  p.subtype x = x
                                                  @[simp]
                                                  theorem SubAddAction.subtype_apply {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} (x : p) :
                                                  p.subtype x = x
                                                  theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
                                                  theorem SubAddAction.subtype_eq_val {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) :
                                                  @[instance 75]
                                                  instance SubMulAction.SMulMemClass.toMulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
                                                  MulAction R S'

                                                  A SubMulAction of a MulAction is a MulAction.

                                                  Equations
                                                    @[instance 75]
                                                    instance SubAddAction.SMulMemClass.toAddAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) :
                                                    AddAction R S'

                                                    A SubAddAction of an AddAction is an AddAction.

                                                    Equations
                                                      def SubMulAction.SMulMemClass.subtype {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
                                                      S' →ₑ[id] M

                                                      The natural MulActionHom over R from a SubMulAction of M to M.

                                                      Equations
                                                        Instances For
                                                          def SubAddAction.SMulMemClass.subtype {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) :
                                                          S' →ₑ[id] M

                                                          The natural AddActionHom over R from a SubAddAction of M to M.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem SubMulAction.SMulMemClass.subtype_apply {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] {S' : A} (x : S') :
                                                              theorem SubMulAction.SMulMemClass.subtype_injective {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
                                                              @[simp]
                                                              theorem SubMulAction.SMulMemClass.coe_subtype {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
                                                              @[simp]
                                                              theorem SubAddAction.SMulMemClass.coe_subtype {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) :
                                                              @[deprecated SubMulAction.SMulMemClass.coe_subtype (since := "2025-02-18")]
                                                              theorem SubMulAction.SMulMemClass.coeSubtype {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :

                                                              Alias of SubMulAction.SMulMemClass.coe_subtype.

                                                              @[deprecated SubAddAction.SMulMemClass.coe_subtype (since := "2025-02-18")]
                                                              theorem SubAddAction.SMulMemClass.coeSubtype {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) :

                                                              Alias of SubAddAction.SMulMemClass.coe_subtype.

                                                              theorem SubMulAction.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M} (h : x p) :
                                                              s x p
                                                              theorem SubAddAction.vadd_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) (s : S) {x : M} (h : x p) :
                                                              s +ᵥ x p
                                                              instance SubMulAction.smul' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) :
                                                              SMul S p
                                                              Equations
                                                                instance SubAddAction.vadd' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) :
                                                                VAdd S p
                                                                Equations
                                                                  instance SubMulAction.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) :
                                                                  IsScalarTower S R p
                                                                  instance SubAddAction.vaddAssocClass {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) :
                                                                  instance SubMulAction.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) {S' : Type u_1} [SMul S' R] [SMul S' S] [SMul S' M] [IsScalarTower S' R M] [IsScalarTower S' S M] :
                                                                  IsScalarTower S' S p
                                                                  instance SubAddAction.vaddAssocClass' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) {S' : Type u_1} [VAdd S' R] [VAdd S' S] [VAdd S' M] [VAddAssocClass S' R M] [VAddAssocClass S' S M] :
                                                                  VAddAssocClass S' S p
                                                                  @[simp]
                                                                  theorem SubMulAction.val_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : p) :
                                                                  ↑(s x) = s x
                                                                  @[simp]
                                                                  theorem SubAddAction.val_vadd_of_tower {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) (s : S) (x : p) :
                                                                  ↑(s +ᵥ x) = s +ᵥ x
                                                                  @[simp]
                                                                  theorem SubMulAction.smul_mem_iff' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] (p : SubMulAction R M) {G : Type u_1} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} :
                                                                  g x p x p
                                                                  @[simp]
                                                                  theorem SubAddAction.vadd_mem_iff' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] (p : SubAddAction R M) {G : Type u_1} [AddGroup G] [VAdd G R] [AddAction G M] [VAddAssocClass G R M] (g : G) {x : M} :
                                                                  g +ᵥ x p x p
                                                                  instance SubMulAction.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
                                                                  instance SubAddAction.isCentralVAdd {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) [VAdd Sᵃᵒᵖ R] [VAdd Sᵃᵒᵖ M] [VAddAssocClass Sᵃᵒᵖ R M] [IsCentralVAdd S M] :
                                                                  instance SubMulAction.mulAction' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) :
                                                                  MulAction S p

                                                                  If the scalar product forms a MulAction, then the subset inherits this action

                                                                  Equations
                                                                    instance SubAddAction.addAction' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S R] [AddAction S M] [VAddAssocClass S R M] (p : SubAddAction R M) :
                                                                    AddAction S p
                                                                    Equations
                                                                      instance SubMulAction.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] (p : SubMulAction R M) :
                                                                      MulAction R p
                                                                      Equations
                                                                        instance SubAddAction.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] (p : SubAddAction R M) :
                                                                        AddAction R p
                                                                        Equations
                                                                          theorem SubMulAction.val_image_orbit {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : p) :

                                                                          Orbits in a SubMulAction coincide with orbits in the ambient space.

                                                                          theorem SubMulAction.mem_orbit_subMul_iff {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} {x m : p} :
                                                                          theorem SubAddAction.mem_orbit_subAdd_iff {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} {x m : p} :

                                                                          Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

                                                                          theorem SubMulAction.stabilizer_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] {p : SubMulAction R M} (m : p) :

                                                                          Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

                                                                          instance SubMulAction.instHasCompl {R : Type u} {M : Type v} [Group R] [MulAction R M] :

                                                                          SubMulAction on the complement of an invariant subset

                                                                          Equations
                                                                            theorem SubMulAction.compl_def {R : Type u} {M : Type v} [Group R] [MulAction R M] (s : SubMulAction R M) :
                                                                            s.carrier = (↑s)
                                                                            theorem SubMulAction.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) (h : (↑p).Nonempty) :
                                                                            0 p
                                                                            instance SubMulAction.instZeroSubtypeMemOfNonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) [n_empty : Nonempty p] :
                                                                            Zero p

                                                                            If the scalar product forms a Module, and the SubMulAction is not , then the subset inherits the zero.

                                                                            Equations
                                                                              theorem SubMulAction.neg_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) {x : M} (hx : x p) :
                                                                              -x p
                                                                              @[simp]
                                                                              theorem SubMulAction.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) {x : M} :
                                                                              -x p x p
                                                                              instance SubMulAction.instNegSubtypeMem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) :
                                                                              Neg p
                                                                              Equations
                                                                                @[simp]
                                                                                theorem SubMulAction.val_neg {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) (x : p) :
                                                                                ↑(-x) = -x
                                                                                theorem SubMulAction.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [GroupWithZero S] [Monoid R] [MulAction R M] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M} (s0 : s 0) :
                                                                                s x p x p
                                                                                def SubMulAction.inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
                                                                                s →ₑ[id] α

                                                                                The inclusion of a SubMulAction into the ambient set, as an equivariant map

                                                                                Equations
                                                                                  Instances For
                                                                                    def SubAddAction.inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) :
                                                                                    s →ₑ[id] α

                                                                                    The inclusion of a SubAddAction into the ambient set, as an equivariant map.

                                                                                    Equations
                                                                                      Instances For
                                                                                        theorem SubMulAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
                                                                                        theorem SubAddAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) :
                                                                                        theorem SubMulAction.image_inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
                                                                                        theorem SubAddAction.image_inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) :

                                                                                        The non-zero elements of M are invariant under the action by the units of R.

                                                                                        Equations
                                                                                          Instances For
                                                                                            instance Units.instMulActionSubtypeNeOfNat (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] :
                                                                                            MulAction Rˣ { x : M // x 0 }
                                                                                            Equations
                                                                                              @[simp]
                                                                                              theorem Units.smul_coe (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (a : Rˣ) (x : { x : M // x 0 }) :
                                                                                              ↑(a x) = a x
                                                                                              theorem Units.orbitRel_nonZero_iff (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (x y : { v : M // v 0 }) :
                                                                                              (MulAction.orbitRel Rˣ { v : M // v 0 }) x y (MulAction.orbitRel Rˣ M) x y