Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2020 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser

! This file was ported from Lean 3 source module group_theory.group_action.sub_mul_action
! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.GroupAction
import Mathlib.Algebra.Module.Basic
import Mathlib.Data.SetLike.Basic
import Mathlib.GroupTheory.GroupAction.Basic

/-!

# 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

* `SubMulAction.mulAction` - the `MulAction R M` transferred to the subtype.
* `SubMulAction.mulAction'` - the `MulAction S M` transferred to the subtype when
  `IsScalarTower S R M`.
* `SubMulAction.isScalarTower` - the `IsScalarTower S R M` transferred to the subtype.

## Tags

submodule, mul_action
-/


open Function

universe u u' u'' v

variable {
S: Type u'
S : 
Type u': Type (u'+1)
Type u'} {
T: Type u''
T : 
Type u'': Type (u''+1)
Type u''} {
R: Type u
R : 
Type u: Type (u+1)
Type u} {
M: Type v
M : 
Type v: Type (v+1)
Type v}

/-- `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.
-/
class 
SMulMemClass: (S : Type u_1) β†’ (R : outParam (Type u_2)) β†’ (M : Type u_3) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass (
S: Type ?u.18
S : 
Type _: Type (?u.18+1)
Type _) (
R: outParam (Type ?u.22)
R : 
outParam: Sort ?u.21 β†’ Sort ?u.21
outParam <| 
Type _: Type (?u.22+1)
Type _) (
M: Type ?u.25
M : 
Type _: Type (?u.25+1)
Type _) [
SMul: Type ?u.29 β†’ Type ?u.28 β†’ Type (max?u.29?u.28)
SMul 
R: outParam (Type ?u.22)
R 
M: Type ?u.25
M] [
SetLike: Type ?u.33 β†’ outParam (Type ?u.32) β†’ Type (max?u.33?u.32)
SetLike 
S: Type ?u.18
S 
M: Type ?u.25
M] where
  /-- Multiplication by a scalar on an element of the set remains in the set. -/
  
smul_mem: βˆ€ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : SMul R M] [inst_1 : SetLike S M]
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r β€’ m ∈ s
smul_mem : βˆ€ {
s: S
s : 
S: Type ?u.18
S} (
r: R
r : 
R: outParam (Type ?u.22)
R) {
m: M
m : 
M: Type ?u.25
M}, 
m: M
m ∈ 
s: S
s β†’ 
r: R
r β€’ 
m: M
m ∈ 
s: S
s
#align smul_mem_class 
SMulMemClass: (S : Type u_1) β†’ (R : outParam (Type u_2)) β†’ (M : Type u_3) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass

/-- `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. -/
class 
VAddMemClass: {S : Type u_1} β†’
  {R : outParam (Type u_2)} β†’
    {M : Type u_3} β†’
      [inst : VAdd R M] β†’ [inst_1 : SetLike S M] β†’ (βˆ€ {s : S} (r : R) {m : M}, m ∈ s β†’ r +α΅₯ m ∈ s) β†’ VAddMemClass S R M
VAddMemClass (
S: Type ?u.163
S : 
Type _: Type (?u.163+1)
Type _) (
R: outParam (Type ?u.167)
R : 
outParam: Sort ?u.166 β†’ Sort ?u.166
outParam <| 
Type _: Type (?u.167+1)
Type _) (
M: Type ?u.170
M : 
Type _: Type (?u.170+1)
Type _) [
VAdd: Type ?u.174 β†’ Type ?u.173 β†’ Type (max?u.174?u.173)
VAdd 
R: outParam (Type ?u.167)
R 
M: Type ?u.170
M] [
SetLike: Type ?u.178 β†’ outParam (Type ?u.177) β†’ Type (max?u.178?u.177)
SetLike 
S: Type ?u.163
S 
M: Type ?u.170
M] where
  /-- Addition by a scalar with an element of the set remains in the set. -/
  
vadd_mem: βˆ€ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : VAdd R M] [inst_1 : SetLike S M]
  [self : VAddMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r +α΅₯ m ∈ s
vadd_mem : βˆ€ {
s: S
s : 
S: Type ?u.163
S} (
r: R
r : 
R: outParam (Type ?u.167)
R) {
m: M
m : 
M: Type ?u.170
M}, 
m: M
m ∈ 
s: S
s β†’ 
r: R
r +α΅₯ 
m: M
m ∈ 
s: S
s
#align vadd_mem_class 
VAddMemClass: (S : Type u_1) β†’ (R : outParam (Type u_2)) β†’ (M : Type u_3) β†’ [inst : VAdd R M] β†’ [inst : SetLike S M] β†’ Type
VAddMemClass

attribute [
to_additive: (S : Type u_1) β†’ (R : outParam (Type u_2)) β†’ (M : Type u_3) β†’ [inst : VAdd R M] β†’ [inst : SetLike S M] β†’ Type
to_additive] 
SMulMemClass: (S : Type u_1) β†’ (R : outParam (Type u_2)) β†’ (M : Type u_3) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass

namespace SetLike

variable [
SMul: Type ?u.1093 β†’ Type ?u.1092 β†’ Type (max?u.1093?u.1092)
SMul 
R: Type u
R 
M: Type v
M] [
SetLike: Type ?u.1097 β†’ outParam (Type ?u.1096) β†’ Type (max?u.1097?u.1096)
SetLike 
S: Type u'
S 
M: Type v
M] [
hS: SMulMemClass S R M
hS : 
SMulMemClass: (S : Type ?u.321) β†’ (R : outParam (Type ?u.320)) β†’ (M : Type ?u.319) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass 
S: Type u'
S 
R: Type u
R 
M: Type v
M] (
s: S
s : 
S: Type u'
S)

open SMulMemClass

-- lower priority so other instances are found first
/-- A subset closed under the scalar action inherits that action. -/
@[
to_additive: {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : VAdd R M] β†’ [inst_1 : SetLike S M] β†’ [hS : VAddMemClass S R M] β†’ (s : S) β†’ VAdd R { x // x ∈ s }
to_additive "A subset closed under the additive action inherits that action."]
instance (priority := 900) 
smul: {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : SMul R M] β†’ [inst_1 : SetLike S M] β†’ [hS : SMulMemClass S R M] β†’ (s : S) β†’ SMul R { x // x ∈ s }
smul : 
SMul: Type ?u.386 β†’ Type ?u.385 β†’ Type (max?u.386?u.385)
SMul 
R: Type u
R 
s: S
s :=
  ⟨fun 
r: ?m.535
r 
x: ?m.538
x => ⟨
r: ?m.535
r β€’ 
x: ?m.538
x.
1: {Ξ± : Sort ?u.560} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
1, 
smul_mem: βˆ€ {S : Type ?u.591} {R : outParam (Type ?u.590)} {M : Type ?u.589} [inst : SMul R M] [inst_1 : SetLike S M]
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r β€’ m ∈ s
smul_mem 
r: ?m.535
r 
x: ?m.538
x.
2: βˆ€ {Ξ± : Sort ?u.658} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2⟩⟩
#align set_like.has_smul 
SetLike.smul: {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : SMul R M] β†’ [inst_1 : SetLike S M] β†’ [hS : SMulMemClass S R M] β†’ (s : S) β†’ SMul R { x // x ∈ s }
SetLike.smul
#align set_like.has_vadd 
SetLike.vadd: {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : VAdd R M] β†’ [inst_1 : SetLike S M] β†’ [hS : VAddMemClass S R M] β†’ (s : S) β†’ VAdd R { x // x ∈ s }
SetLike.vadd

-- Porting note: TODO lower priority not actually there
-- lower priority so later simp lemmas are used first; to appease simp_nf
@[
to_additive: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), ↑(r +α΅₯ x) = r +α΅₯ ↑x
to_additive (attr := simp, norm_cast)]
protected theorem 
val_smul: βˆ€ (r : R) (x : { x // x ∈ s }), ↑(r β€’ x) = r β€’ ↑x
val_smul (
r: R
r : 
R: Type u
R) (
x: { x // x ∈ s }
x : 
s: S
s) : (↑(
r: R
r β€’ 
x: { x // x ∈ s }
x) : 
M: Type v
M) = 
r: R
r β€’ (
x: { x // x ∈ s }
x : 
M: Type v
M) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.3246} {a : Ξ±}, a = a
rfl
#align set_like.coe_smul 
SetLike.val_smul: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), ↑(r β€’ x) = r β€’ ↑x
SetLike.val_smul
#align set_like.coe_vadd 
SetLike.val_vadd: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), ↑(r +α΅₯ x) = r +α΅₯ ↑x
SetLike.val_vadd

-- Porting note: TODO lower priority not actually there
-- lower priority so later simp lemmas are used first; to appease simp_nf
@[
to_additive: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r +α΅₯ { val := x, property := hx } = { val := r +α΅₯ x, property := (_ : r +α΅₯ x ∈ s) }
to_additive (attr := simp)]
theorem 
mk_smul_mk: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r β€’ { val := x, property := hx } = { val := r β€’ x, property := (_ : r β€’ x ∈ s) }
mk_smul_mk (
r: R
r : 
R: Type u
R) (
x: M
x : 
M: Type v
M) (
hx: x ∈ s
hx : 
x: M
x ∈ 
s: S
s) : 
r: R
r β€’ (⟨
x: M
x, 
hx: x ∈ s
hx⟩ : 
s: S
s) = ⟨
r: R
r β€’ 
x: M
x, 
smul_mem: βˆ€ {S : Type ?u.5682} {R : outParam (Type ?u.5681)} {M : Type ?u.5680} [inst : SMul R M] [inst_1 : SetLike S M]
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r β€’ m ∈ s
smul_mem 
r: R
r 
hx: x ∈ s
hx⟩ :=
  
rfl: βˆ€ {Ξ± : Sort ?u.5764} {a : Ξ±}, a = a
rfl
#align set_like.mk_smul_mk 
SetLike.mk_smul_mk: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r β€’ { val := x, property := hx } = { val := r β€’ x, property := (_ : r β€’ x ∈ s) }
SetLike.mk_smul_mk
#align set_like.mk_vadd_mk 
SetLike.mk_vadd_mk: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r +α΅₯ { val := x, property := hx } = { val := r +α΅₯ x, property := (_ : r +α΅₯ x ∈ s) }
SetLike.mk_vadd_mk

@[
to_additive: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), r +α΅₯ x = { val := ↑(r +α΅₯ x), property := (_ : r +α΅₯ ↑x ∈ s) }
to_additive]
theorem 
smul_def: βˆ€ (r : R) (x : { x // x ∈ s }), r β€’ x = { val := ↑(r β€’ x), property := (_ : r β€’ ↑x ∈ s) }
smul_def (
r: R
r : 
R: Type u
R) (
x: { x // x ∈ s }
x : 
s: S
s) : 
r: R
r β€’ 
x: { x // x ∈ s }
x = ⟨
r: R
r β€’ 
x: { x // x ∈ s }
x, 
smul_mem: βˆ€ {S : Type ?u.9600} {R : outParam (Type ?u.9599)} {M : Type ?u.9598} [inst : SMul R M] [inst_1 : SetLike S M]
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r β€’ m ∈ s
smul_mem 
r: R
r 
x: { x // x ∈ s }
x.
2: βˆ€ {Ξ± : Sort ?u.9667} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2⟩ :=
  
rfl: βˆ€ {Ξ± : Sort ?u.9691} {a : Ξ±}, a = a
rfl
#align set_like.smul_def 
SetLike.smul_def: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), r β€’ x = { val := ↑(r β€’ x), property := (_ : r β€’ ↑x ∈ s) }
SetLike.smul_def
#align set_like.vadd_def 
SetLike.vadd_def: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M] [hS : VAddMemClass S R M] (s : S)
  (r : R) (x : { x // x ∈ s }), r +α΅₯ x = { val := ↑(r +α΅₯ x), property := (_ : r +α΅₯ ↑x ∈ s) }
SetLike.vadd_def

@[simp]
theorem 
forall_smul_mem_iff: βˆ€ {R : Type u_1} {M : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SetLike S M]
  [inst_3 : SMulMemClass S R M] {N : S} {x : M}, (βˆ€ (a : R), a β€’ x ∈ N) ↔ x ∈ N
forall_smul_mem_iff {
R: Type u_1
R 
M: Type ?u.9796
M 
S: Type ?u.9799
S : 
Type _: Type (?u.9793+1)
Type _} [
Monoid: Type ?u.9802 β†’ Type ?u.9802
Monoid 
R: Type ?u.9793
R] [
MulAction: (Ξ± : Type ?u.9806) β†’ Type ?u.9805 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.9806?u.9805)
MulAction 
R: Type ?u.9793
R 
M: Type ?u.9796
M] [
SetLike: Type ?u.9819 β†’ outParam (Type ?u.9818) β†’ Type (max?u.9819?u.9818)
SetLike 
S: Type ?u.9799
S 
M: Type ?u.9796
M]
    [
SMulMemClass: (S : Type ?u.9824) β†’
  (R : outParam (Type ?u.9823)) β†’ (M : Type ?u.9822) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass 
S: Type ?u.9799
S 
R: Type ?u.9793
R 
M: Type ?u.9796
M] {
N: S
N : 
S: Type ?u.9799
S} {
x: M
x : 
M: Type ?u.9796
M} : (βˆ€ 
a: R
a : 
R: Type ?u.9793
R, 
a: R
a β€’ 
x: M
x ∈ 
N: S
N) ↔ 
x: M
x ∈ 
N: S
N :=
  ⟨fun 
h: ?m.11175
h => 
Goals accomplished! πŸ™
S✝: Type u'

T: Type u''

R✝: Type u

M✝: Type v

inst✝⁡: SMul R✝ M✝

inst✝⁴: SetLike S✝ M✝

hS: SMulMemClass S✝ R✝ M✝

s: S✝

R: Type u_1

M: Type u_2

S: Type u_3

inst✝³: Monoid R

inst✝²: MulAction R M

inst✝¹: SetLike S M

inst✝: SMulMemClass S R M

N: S

x: M

h: βˆ€ (a : R), a β€’ x ∈ N

x ∈ N
Goals accomplished! πŸ™
, fun 
h: ?m.11185
h 
a: ?m.11188
a => 
SMulMemClass.smul_mem: βˆ€ {S : Type ?u.11192} {R : outParam (Type ?u.11191)} {M : Type ?u.11190} [inst : SMul R M] [inst_1 : SetLike S M]
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s β†’ r β€’ m ∈ s
SMulMemClass.smul_mem 
a: ?m.11188
a 
h: ?m.11185
h⟩
#align set_like.forall_smul_mem_iff 
SetLike.forall_smul_mem_iff: βˆ€ {R : Type u_1} {M : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SetLike S M]
  [inst_3 : SMulMemClass S R M] {N : S} {x : M}, (βˆ€ (a : R), a β€’ x ∈ N) ↔ x ∈ N
SetLike.forall_smul_mem_iff

end SetLike

/-- A SubMulAction is a set which is closed under scalar multiplication.  -/
structure 
SubMulAction: {R : Type u} β†’
  {M : Type v} β†’
    [inst : SMul R M] β†’ (carrier : Set M) β†’ (βˆ€ (c : R) {x : M}, x ∈ carrier β†’ c β€’ x ∈ carrier) β†’ SubMulAction R M
SubMulAction (
R: Type u
R : 
Type u: Type (u+1)
Type u) (
M: Type v
M : 
Type v: Type (v+1)
Type v) [
SMul: Type ?u.12566 β†’ Type ?u.12565 β†’ Type (max?u.12566?u.12565)
SMul 
R: Type u
R 
M: Type v
M] : 
Type v: Type (v+1)
Type v where
  /-- The underlying set of a `SubMulAction`. -/
  
carrier: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ SubMulAction R M β†’ Set M
carrier : 
Set: Type ?u.12570 β†’ Type ?u.12570
Set 
M: Type v
M
  /-- The carrier set is closed under scalar multiplication. -/
  
smul_mem': βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
  x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
smul_mem' : βˆ€ (
c: R
c : 
R: Type u
R) {
x: M
x : 
M: Type v
M}, 
x: M
x ∈ 
carrier: Set M
carrier β†’ 
c: R
c β€’ 
x: M
x ∈ 
carrier: Set M
carrier
#align sub_mul_action 
SubMulAction: (R : Type u) β†’ (M : Type v) β†’ [inst : SMul R M] β†’ Type v
SubMulAction

namespace SubMulAction

variable [
SMul: Type ?u.13591 β†’ Type ?u.13590 β†’ Type (max?u.13591?u.13590)
SMul 
R: Type u
R 
M: Type v
M]


instance: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ SetLike (SubMulAction R M) M
instance : 
SetLike: Type ?u.13098 β†’ outParam (Type ?u.13097) β†’ Type (max?u.13098?u.13097)
SetLike (
SubMulAction: (R : Type ?u.13100) β†’ (M : Type ?u.13099) β†’ [inst : SMul R M] β†’ Type ?u.13099
SubMulAction 
R: Type u
R 
M: Type v
M) 
M: Type v
M :=
  ⟨
SubMulAction.carrier: {R : Type ?u.13125} β†’ {M : Type ?u.13124} β†’ [inst : SMul R M] β†’ SubMulAction R M β†’ Set M
SubMulAction.carrier, fun 
p: ?m.13187
p 
q: ?m.13190
q 
h: ?m.13193
h => 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p, q: SubMulAction R M

h: p.carrier = q.carrier

p = q
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

q: SubMulAction R M

carrier✝: Set M

smul_mem'✝: βˆ€ (c : R) {x : M}, x ∈ carrier✝ β†’ c β€’ x ∈ carrier✝

h: { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier = q.carrier

mk
{ carrier := carrier✝, smul_mem' := smul_mem'✝ } = q
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

q: SubMulAction R M

carrier✝: Set M

smul_mem'✝: βˆ€ (c : R) {x : M}, x ∈ carrier✝ β†’ c β€’ x ∈ carrier✝

h: { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier = q.carrier

mk
{ carrier := carrier✝, smul_mem' := smul_mem'✝ } = q
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p, q: SubMulAction R M

h: p.carrier = q.carrier

p = q
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

carrier✝¹: Set M

smul_mem'✝¹: βˆ€ (c : R) {x : M}, x ∈ carrier✝¹ β†’ c β€’ x ∈ carrier✝¹

carrier✝: Set M

smul_mem'✝: βˆ€ (c : R) {x : M}, x ∈ carrier✝ β†’ c β€’ x ∈ carrier✝

h: { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier

mk.mk
{ carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

carrier✝¹: Set M

smul_mem'✝¹: βˆ€ (c : R) {x : M}, x ∈ carrier✝¹ β†’ c β€’ x ∈ carrier✝¹

carrier✝: Set M

smul_mem'✝: βˆ€ (c : R) {x : M}, x ∈ carrier✝ β†’ c β€’ x ∈ carrier✝

h: { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier

mk.mk
{ carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p, q: SubMulAction R M

h: p.carrier = q.carrier

p = q
Goals accomplished! πŸ™
 ⟩


instance: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ SMulMemClass (SubMulAction R M) R M
instance : 
SMulMemClass: (S : Type ?u.13596) β†’
  (R : outParam (Type ?u.13595)) β†’ (M : Type ?u.13594) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass (
SubMulAction: (R : Type ?u.13598) β†’ (M : Type ?u.13597) β†’ [inst : SMul R M] β†’ Type ?u.13597
SubMulAction 
R: Type u
R 
M: Type v
M) 
R: Type u
R 
M: Type v
M where smul_mem := 
smul_mem': βˆ€ {R : Type ?u.13644} {M : Type ?u.13643} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
  x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
smul_mem' 
_: SubMulAction ?m.13645 ?m.13646
_

@[simp]
theorem 
mem_carrier: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} {x : M}, x ∈ p.carrier ↔ x ∈ ↑p
mem_carrier {
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.13808) β†’ (M : Type ?u.13807) β†’ [inst : SMul R M] β†’ Type ?u.13807
SubMulAction 
R: Type u
R 
M: Type v
M} {
x: M
x : 
M: Type v
M} : 
x: M
x ∈ 
p: SubMulAction R M
p.
carrier: {R : Type ?u.13830} β†’ {M : Type ?u.13829} β†’ [inst : SMul R M] β†’ SubMulAction R M β†’ Set M
carrier ↔ 
x: M
x ∈ (
p: SubMulAction R M
p : 
Set: Type ?u.13856 β†’ Type ?u.13856
Set 
M: Type v
M) :=
  
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align sub_mul_action.mem_carrier 
SubMulAction.mem_carrier: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} {x : M}, x ∈ p.carrier ↔ x ∈ ↑p
SubMulAction.mem_carrier

@[ext]
theorem 
ext: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p q : SubMulAction R M}, (βˆ€ (x : M), x ∈ p ↔ x ∈ q) β†’ p = q
ext {
p: SubMulAction R M
p 
q: SubMulAction R M
q : 
SubMulAction: (R : Type ?u.14021) β†’ (M : Type ?u.14020) β†’ [inst : SMul R M] β†’ Type ?u.14020
SubMulAction 
R: Type u
R 
M: Type v
M} (
h: βˆ€ (x : M), x ∈ p ↔ x ∈ q
h : βˆ€ 
x: ?m.14026
x, 
x: ?m.14026
x ∈ 
p: SubMulAction R M
p ↔ 
x: ?m.14026
x ∈ 
q: SubMulAction R M
q) : 
p: SubMulAction R M
p = 
q: SubMulAction R M
q :=
  
SetLike.ext: βˆ€ {A : Type ?u.14096} {B : Type ?u.14095} [i : SetLike A B] {p q : A}, (βˆ€ (x : B), x ∈ p ↔ x ∈ q) β†’ p = q
SetLike.ext 
h: βˆ€ (x : M), x ∈ p ↔ x ∈ q
h
#align sub_mul_action.ext 
SubMulAction.ext: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p q : SubMulAction R M}, (βˆ€ (x : M), x ∈ p ↔ x ∈ q) β†’ p = q
SubMulAction.ext

/-- Copy of a sub_mul_action with a new `carrier` equal to the old one. Useful to fix definitional
equalities.-/
protected def 
copy: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ (s : Set M) β†’ s = ↑p β†’ SubMulAction R M
copy (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.14169) β†’ (M : Type ?u.14168) β†’ [inst : SMul R M] β†’ Type ?u.14168
SubMulAction 
R: Type u
R 
M: Type v
M) (
s: Set M
s : 
Set: Type ?u.14183 β†’ Type ?u.14183
Set 
M: Type v
M) (
hs: s = ↑p
hs : 
s: Set M
s = ↑
p: SubMulAction R M
p) : 
SubMulAction: (R : Type ?u.14293) β†’ (M : Type ?u.14292) β†’ [inst : SMul R M] β†’ Type ?u.14292
SubMulAction 
R: Type u
R 
M: Type v
M
    where
  carrier := 
s: Set M
s
  smul_mem' := 
hs: s = ↑p
hs.
symm: βˆ€ {Ξ± : Sort ?u.14306} {a b : Ξ±}, a = b β†’ b = a
symm β–Έ 
p: SubMulAction R M
p.
smul_mem': βˆ€ {R : Type ?u.14318} {M : Type ?u.14317} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
  x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
smul_mem'
#align sub_mul_action.copy 
SubMulAction.copy: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ (s : Set M) β†’ s = ↑p β†’ SubMulAction R M
SubMulAction.copy

@[simp]
theorem 
coe_copy: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p),
  ↑(SubMulAction.copy p s hs) = s
coe_copy (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.14437) β†’ (M : Type ?u.14436) β†’ [inst : SMul R M] β†’ Type ?u.14436
SubMulAction 
R: Type u
R 
M: Type v
M) (
s: Set M
s : 
Set: Type ?u.14451 β†’ Type ?u.14451
Set 
M: Type v
M) (
hs: s = ↑p
hs : 
s: Set M
s = ↑
p: SubMulAction R M
p) : (
p: SubMulAction R M
p.
copy: {R : Type ?u.14564} β†’
  {M : Type ?u.14563} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ (s : Set M) β†’ s = ↑p β†’ SubMulAction R M
copy 
s: Set M
s 
hs: s = ?m.14458
hs : 
Set: Type ?u.14562 β†’ Type ?u.14562
Set 
M: Type v
M) = 
s: Set M
s :=
  
rfl: βˆ€ {Ξ± : Sort ?u.14653} {a : Ξ±}, a = a
rfl
#align sub_mul_action.coe_copy 
SubMulAction.coe_copy: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p),
  ↑(SubMulAction.copy p s hs) = s
SubMulAction.coe_copy

theorem 
copy_eq: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p),
  SubMulAction.copy p s hs = p
copy_eq (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.14702) β†’ (M : Type ?u.14701) β†’ [inst : SMul R M] β†’ Type ?u.14701
SubMulAction 
R: Type u
R 
M: Type v
M) (
s: Set M
s : 
Set: Type ?u.14716 β†’ Type ?u.14716
Set 
M: Type v
M) (
hs: s = ↑p
hs : 
s: Set M
s = ↑
p: SubMulAction R M
p) : 
p: SubMulAction R M
p.
copy: {R : Type ?u.14827} β†’
  {M : Type ?u.14826} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ (s : Set M) β†’ s = ↑p β†’ SubMulAction R M
copy 
s: Set M
s 
hs: s = ?m.14723
hs = 
p: SubMulAction R M
p :=
  
SetLike.coe_injective: βˆ€ {A : Type ?u.14847} {B : Type ?u.14848} [i : SetLike A B], Injective SetLike.coe
SetLike.coe_injective 
hs: s = ↑p
hs
#align sub_mul_action.copy_eq 
SubMulAction.copy_eq: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p),
  SubMulAction.copy p s hs = p
SubMulAction.copy_eq


instance: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ Bot (SubMulAction R M)
instance : 
Bot: Type ?u.14908 β†’ Type ?u.14908
Bot (
SubMulAction: (R : Type ?u.14910) β†’ (M : Type ?u.14909) β†’ [inst : SMul R M] β†’ Type ?u.14909
SubMulAction 
R: Type u
R 
M: Type v
M) where
  bot :=
    { carrier := 
βˆ…: ?m.14935
βˆ…
      smul_mem' := fun 
_c: ?m.14981
_c 
h: ?m.14984
h => 
Set.not_mem_empty: βˆ€ {Ξ± : Type ?u.14986} (x : Ξ±), Β¬x ∈ βˆ…
Set.not_mem_empty 
h: ?m.14984
h }


instance: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ Inhabited (SubMulAction R M)
instance : 
Inhabited: Sort ?u.15062 β†’ Sort (max1?u.15062)
Inhabited (
SubMulAction: (R : Type ?u.15064) β†’ (M : Type ?u.15063) β†’ [inst : SMul R M] β†’ Type ?u.15063
SubMulAction 
R: Type u
R 
M: Type v
M) :=
  ⟨
βŠ₯: ?m.15083
βŠ₯⟩

end SubMulAction

namespace SubMulAction

section SMul

variable [
SMul: Type ?u.15434 β†’ Type ?u.15433 β†’ Type (max?u.15434?u.15433)
SMul 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.15890) β†’ (M : Type ?u.15889) β†’ [inst : SMul R M] β†’ Type ?u.15889
SubMulAction 
R: Type u
R 
M: Type v
M)

variable {
r: R
r : 
R: Type u
R} {
x: M
x : 
M: Type v
M}

theorem 
smul_mem: βˆ€ (r : R), x ∈ p β†’ r β€’ x ∈ p
smul_mem (
r: R
r : 
R: Type u
R) (
h: x ∈ p
h : 
x: M
x ∈ 
p: SubMulAction R M
p) : 
r: R
r β€’ 
x: M
x ∈ 
p: SubMulAction R M
p :=
  
p: SubMulAction R M
p.
smul_mem': βˆ€ {R : Type ?u.15391} {M : Type ?u.15390} [inst : SMul R M] (self : SubMulAction R M) (c : R) {x : M},
  x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
smul_mem' 
r: R
r 
h: x ∈ p
h
#align sub_mul_action.smul_mem 
SubMulAction.smul_mem: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x ∈ p β†’ r β€’ x ∈ p
SubMulAction.smul_mem


instance: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ SMul R { x // x ∈ p }
instance : 
SMul: Type ?u.15457 β†’ Type ?u.15456 β†’ Type (max?u.15457?u.15456)
SMul 
R: Type u
R 
p: SubMulAction R M
p where smul 
c: ?m.15617
c 
x: ?m.15620
x := ⟨
c: ?m.15617
c β€’ 
x: ?m.15620
x.
1: {Ξ± : Sort ?u.15642} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
1, 
smul_mem: βˆ€ {R : Type ?u.15670} {M : Type ?u.15669} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x ∈ p β†’ r β€’ x ∈ p
smul_mem 
_: SubMulAction ?m.15671 ?m.15672
_ 
c: ?m.15617
c 
x: ?m.15620
x.
2: βˆ€ {Ξ± : Sort ?u.15719} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2⟩

variable {
p: ?m.15908
p}

@[simp, norm_cast]
theorem 
val_smul: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : { x // x ∈ p }), ↑(r β€’ x) = r β€’ ↑x
val_smul (
r: R
r : 
R: Type u
R) (
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : (↑(
r: R
r β€’ 
x: { x // x ∈ p }
x) : 
M: Type v
M) = 
r: R
r β€’ (
x: { x // x ∈ p }
x : 
M: Type v
M) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16235} {a : Ξ±}, a = a
rfl
#align sub_mul_action.coe_smul 
SubMulAction.val_smul: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : { x // x ∈ p }), ↑(r β€’ x) = r β€’ ↑x
SubMulAction.val_smul

-- porting note: no longer needed because of defeq structure eta
#noalign sub_mul_action.coe_mk

variable (
p: ?m.16409
p)

/-- Embedding of a submodule `p` to the ambient space `M`. -/
protected def 
subtype: { x // x ∈ p } β†’[R] M
subtype : 
p: SubMulAction R M
p β†’[
R: Type u
R] 
M: Type v
M := 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p: SubMulAction R M

r: R

x: M

{ x // x ∈ p } β†’[R] M
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p: SubMulAction R M

r: R

x: M

βˆ€ (m : R) (x : { x // x ∈ p }), ↑(m β€’ x) = m β€’ ↑x
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p: SubMulAction R M

r: R

x: M

βˆ€ (m : R) (x : { x // x ∈ p }), ↑(m β€’ x) = m β€’ ↑x
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝: SMul R M

p: SubMulAction R M

r: R

x: M

{ x // x ∈ p } β†’[R] M
Goals accomplished! πŸ™

#align sub_mul_action.subtype 
SubMulAction.subtype: {R : Type u} β†’ {M : Type v} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ { x // x ∈ p } β†’[R] M
SubMulAction.subtype

@[simp]
theorem 
subtype_apply: βˆ€ (x : { x // x ∈ p }), ↑(SubMulAction.subtype p) x = ↑x
subtype_apply (
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : 
p: SubMulAction R M
p.
subtype: {R : Type ?u.20577} β†’ {M : Type ?u.20576} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ { x // x ∈ p } β†’[R] M
subtype 
x: { x // x ∈ p }
x = 
x: { x // x ∈ p }
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.20896} {a : Ξ±}, a = a
rfl
#align sub_mul_action.subtype_apply 
SubMulAction.subtype_apply: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (x : { x // x ∈ p }),
  ↑(SubMulAction.subtype p) x = ↑x
SubMulAction.subtype_apply

theorem 
subtype_eq_val: ↑(SubMulAction.subtype p) = Subtype.val
subtype_eq_val : (
SubMulAction.subtype: {R : Type ?u.21012} β†’ {M : Type ?u.21011} β†’ [inst : SMul R M] β†’ (p : SubMulAction R M) β†’ { x // x ∈ p } β†’[R] M
SubMulAction.subtype 
p: SubMulAction R M
p : 
p: SubMulAction R M
p β†’ 
M: Type v
M) = 
Subtype.val: {Ξ± : Sort ?u.21158} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
Subtype.val :=
  
rfl: βˆ€ {Ξ± : Sort ?u.21211} {a : Ξ±}, a = a
rfl
#align sub_mul_action.subtype_eq_val 
SubMulAction.subtype_eq_val: βˆ€ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M), ↑(SubMulAction.subtype p) = Subtype.val
SubMulAction.subtype_eq_val

end SMul

namespace SMulMemClass

variable [
Monoid: Type ?u.26480 β†’ Type ?u.26480
Monoid 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.26484) β†’ Type ?u.26483 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.26484?u.26483)
MulAction 
R: Type u
R 
M: Type v
M] {
A: Type ?u.21284
A : 
Type _: Type (?u.21253+1)
Type _} [
SetLike: Type ?u.21257 β†’ outParam (Type ?u.21256) β†’ Type (max?u.21257?u.21256)
SetLike 
A: Type ?u.21253
A 
M: Type v
M]

variable [
hA: SMulMemClass A R M
hA : 
SMulMemClass: (S : Type ?u.22041) β†’
  (R : outParam (Type ?u.22040)) β†’ (M : Type ?u.22039) β†’ [inst : SMul R M] β†’ [inst : SetLike S M] β†’ Type
SMulMemClass 
A: Type ?u.21284
A 
R: Type u
R 
M: Type v
M] (
S': A
S' : 
A: Type ?u.21284
A)

-- Prefer subclasses of `MulAction` over `SMulMemClass`.
/-- A `SubMulAction` of a `MulAction` is a `MulAction`.  -/
instance (priority := 75) 
toMulAction: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Monoid R] β†’
      [inst_1 : MulAction R M] β†’
        {A : Type u_1} β†’ [inst_2 : SetLike A M] β†’ [hA : SMulMemClass A R M] β†’ (S' : A) β†’ MulAction R { x // x ∈ S' }
toMulAction : 
MulAction: (Ξ± : Type ?u.22757) β†’ Type ?u.22756 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.22757?u.22756)
MulAction 
R: Type u
R 
S': A
S' :=
  
Subtype.coe_injective: βˆ€ {Ξ± : Sort ?u.22905} {p : Ξ± β†’ Prop}, Injective fun a => ↑a
Subtype.coe_injective.
mulAction: {M : Type ?u.22910} β†’
  {Ξ± : Type ?u.22909} β†’
    {Ξ² : Type ?u.22908} β†’
      [inst : Monoid M] β†’
        [inst_1 : MulAction M Ξ±] β†’
          [inst_2 : SMul M Ξ²] β†’ (f : Ξ² β†’ Ξ±) β†’ Injective f β†’ (βˆ€ (c : M) (x : Ξ²), f (c β€’ x) = c β€’ f x) β†’ MulAction M Ξ²
mulAction 
Subtype.val: {Ξ± : Sort ?u.23043} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
Subtype.val (
SetLike.val_smul: βˆ€ {S : Type ?u.23063} {R : Type ?u.23064} {M : Type ?u.23062} [inst : SMul R M] [inst_1 : SetLike S M]
  [hS : SMulMemClass S R M] (s : S) (r : R) (x : { x // x ∈ s }), ↑(r β€’ x) = r β€’ ↑x
SetLike.val_smul 
S': A
S')
#align sub_mul_action.smul_mem_class.to_mul_action 
SubMulAction.SMulMemClass.toMulAction: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Monoid R] β†’
      [inst_1 : MulAction R M] β†’
        {A : Type u_1} β†’ [inst_2 : SetLike A M] β†’ [hA : SMulMemClass A R M] β†’ (S' : A) β†’ MulAction R { x // x ∈ S' }
SubMulAction.SMulMemClass.toMulAction

/-- The natural `MulActionHom` over `R` from a `SubMulAction` of `M` to `M`. -/
protected def 
subtype: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Monoid R] β†’
      [inst_1 : MulAction R M] β†’
        {A : Type u_1} β†’ [inst_2 : SetLike A M] β†’ [hA : SMulMemClass A R M] β†’ (S' : A) β†’ { x // x ∈ S' } β†’[R] M
subtype : 
S': A
S' β†’[
R: Type u
R] 
M: Type v
M :=
  ⟨
Subtype.val: {Ξ± : Sort ?u.30272} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
Subtype.val, fun 
_: ?m.30284
_ 
_: ?m.30287
_ => 
rfl: βˆ€ {Ξ± : Sort ?u.30289} {a : Ξ±}, a = a
rfl⟩
#align sub_mul_action.smul_mem_class.subtype 
SubMulAction.SMulMemClass.subtype: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Monoid R] β†’
      [inst_1 : MulAction R M] β†’
        {A : Type u_1} β†’ [inst_2 : SetLike A M] β†’ [hA : SMulMemClass A R M] β†’ (S' : A) β†’ { x // x ∈ S' } β†’[R] M
SubMulAction.SMulMemClass.subtype

@[simp]
protected theorem 
coeSubtype: βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), ↑(SMulMemClass.subtype S') = Subtype.val
coeSubtype : (
SMulMemClass.subtype: {R : Type ?u.31170} β†’
  {M : Type ?u.31169} β†’
    [inst : Monoid R] β†’
      [inst_1 : MulAction R M] β†’
        {A : Type ?u.31168} β†’ [inst_2 : SetLike A M] β†’ [hA : SMulMemClass A R M] β†’ (S' : A) β†’ { x // x ∈ S' } β†’[R] M
SMulMemClass.subtype 
S': A
S' : 
S': A
S' β†’ 
M: Type v
M) = 
Subtype.val: {Ξ± : Sort ?u.31432} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
Subtype.val :=
  
rfl: βˆ€ {Ξ± : Sort ?u.31493} {a : Ξ±}, a = a
rfl
#align sub_mul_action.smul_mem_class.coe_subtype 
SubMulAction.SMulMemClass.coeSubtype: βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), ↑(SMulMemClass.subtype S') = Subtype.val
SubMulAction.SMulMemClass.coeSubtype

end SMulMemClass

section MulActionMonoid

variable [
Monoid: Type ?u.38384 β†’ Type ?u.38384
Monoid 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.42602) β†’ Type ?u.42601 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.42602?u.42601)
MulAction 
R: Type u
R 
M: Type v
M]

section

variable [
SMul: Type ?u.42615 β†’ Type ?u.42614 β†’ Type (max?u.42615?u.42614)
SMul 
S: Type u'
S 
R: Type u
R] [
SMul: Type ?u.33688 β†’ Type ?u.33687 β†’ Type (max?u.33688?u.33687)
SMul 
S: Type u'
S 
M: Type v
M] [
IsScalarTower: (M : Type ?u.33693) β†’
  (N : Type ?u.33692) β†’ (Ξ± : Type ?u.33691) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S: Type u'
S 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.33105) β†’ (M : Type ?u.33104) β†’ [inst : SMul R M] β†’ Type ?u.33104
SubMulAction 
R: Type u
R 
M: Type v
M)

theorem 
smul_of_tower_mem: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M}, x ∈ p β†’ s β€’ x ∈ p
smul_of_tower_mem (
s: S
s : 
S: Type u'
S) {
x: M
x : 
M: Type v
M} (
h: x ∈ p
h : 
x: M
x ∈ 
p: SubMulAction R M
p) : 
s: S
s β€’ 
x: M
x ∈ 
p: SubMulAction R M
p := 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

s β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

s β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

s β€’ 1 β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

s β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

(s β€’ 1) β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

(s β€’ 1) β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝⁴: Monoid R

inst✝³: MulAction R M

inst✝²: SMul S R

inst✝¹: SMul S M

inst✝: IsScalarTower S R M

p: SubMulAction R M

s: S

x: M

h: x ∈ p

s β€’ x ∈ p
Goals accomplished! πŸ™

#align sub_mul_action.smul_of_tower_mem 
SubMulAction.smul_of_tower_mem: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M}, x ∈ p β†’ s β€’ x ∈ p
SubMulAction.smul_of_tower_mem

instance 
smul': SMul S { x // x ∈ p }
smul' : 
SMul: Type ?u.37675 β†’ Type ?u.37674 β†’ Type (max?u.37675?u.37674)
SMul 
S: Type u'
S 
p: SubMulAction R M
p where smul 
c: ?m.37839
c 
x: ?m.37842
x := ⟨
c: ?m.37839
c β€’ 
x: ?m.37842
x.
1: {Ξ± : Sort ?u.37864} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
1, 
smul_of_tower_mem: βˆ€ {S : Type ?u.37894} {R : Type ?u.37895} {M : Type ?u.37893} [inst : Monoid R] [inst_1 : MulAction R M]
  [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M},
  x ∈ p β†’ s β€’ x ∈ p
smul_of_tower_mem 
_: SubMulAction ?m.37897 ?m.37898
_ 
c: ?m.37839
c 
x: ?m.37842
x.
2: βˆ€ {Ξ± : Sort ?u.38112} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2⟩
#align sub_mul_action.has_smul' 
SubMulAction.smul': {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : Monoid R] β†’
        [inst_1 : MulAction R M] β†’
          [inst_2 : SMul S R] β†’
            [inst_3 : SMul S M] β†’ [inst_4 : IsScalarTower S R M] β†’ (p : SubMulAction R M) β†’ SMul S { x // x ∈ p }
SubMulAction.smul'

instance 
isScalarTower: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M), IsScalarTower S R { x // x ∈ p }
isScalarTower : 
IsScalarTower: (M : Type ?u.39695) β†’
  (N : Type ?u.39694) β†’ (Ξ± : Type ?u.39693) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S: Type u'
S 
R: Type u
R 
p: SubMulAction R M
p where
  smul_assoc 
s: ?m.41808
s 
r: ?m.41811
r 
x: ?m.41814
x := 
Subtype.ext: βˆ€ {Ξ± : Sort ?u.41816} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 β†’ a1 = a2
Subtype.ext <| 
smul_assoc: βˆ€ {Ξ± : Type ?u.41832} {M : Type ?u.41830} {N : Type ?u.41831} [inst : SMul M N] [inst_1 : SMul N Ξ±] [inst_2 : SMul M Ξ±]
  [inst_3 : IsScalarTower M N Ξ±] (x : M) (y : N) (z : Ξ±), (x β€’ y) β€’ z = x β€’ y β€’ z
smul_assoc 
s: ?m.41808
s 
r: ?m.41811
r (
x: ?m.41814
x : 
M: Type v
M)
#align sub_mul_action.is_scalar_tower 
SubMulAction.isScalarTower: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M), IsScalarTower S R { x // x ∈ p }
SubMulAction.isScalarTower

instance 
isScalarTower': βˆ€ {S' : Type ?u.43907} [inst : SMul S' R] [inst_1 : SMul S' S] [inst_2 : SMul S' M] [inst_3 : IsScalarTower S' R M]
  [inst_4 : IsScalarTower S' S M], IsScalarTower S' S { x // x ∈ p }
isScalarTower' {
S': Type ?u.43907
S' : 
Type _: Type (?u.43907+1)
Type _} [
SMul: Type ?u.43911 β†’ Type ?u.43910 β†’ Type (max?u.43911?u.43910)
SMul 
S': Type ?u.43907
S' 
R: Type u
R] [
SMul: Type ?u.43915 β†’ Type ?u.43914 β†’ Type (max?u.43915?u.43914)
SMul 
S': Type ?u.43907
S' 
S: Type u'
S] [
SMul: Type ?u.43919 β†’ Type ?u.43918 β†’ Type (max?u.43919?u.43918)
SMul 
S': Type ?u.43907
S' 
M: Type v
M] [
IsScalarTower: (M : Type ?u.43924) β†’
  (N : Type ?u.43923) β†’ (Ξ± : Type ?u.43922) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S': Type ?u.43907
S' 
R: Type u
R 
M: Type v
M]
    [
IsScalarTower: (M : Type ?u.44656) β†’
  (N : Type ?u.44655) β†’ (Ξ± : Type ?u.44654) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S': Type ?u.43907
S' 
S: Type u'
S 
M: Type v
M] : 
IsScalarTower: (M : Type ?u.44690) β†’
  (N : Type ?u.44689) β†’ (Ξ± : Type ?u.44688) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S': Type ?u.43907
S' 
S: Type u'
S 
p: SubMulAction R M
p
    where smul_assoc 
s: ?m.45141
s 
r: ?m.45144
r 
x: ?m.45147
x := 
Subtype.ext: βˆ€ {Ξ± : Sort ?u.45149} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 β†’ a1 = a2
Subtype.ext <| 
smul_assoc: βˆ€ {Ξ± : Type ?u.45165} {M : Type ?u.45163} {N : Type ?u.45164} [inst : SMul M N] [inst_1 : SMul N Ξ±] [inst_2 : SMul M Ξ±]
  [inst_3 : IsScalarTower M N Ξ±] (x : M) (y : N) (z : Ξ±), (x β€’ y) β€’ z = x β€’ y β€’ z
smul_assoc 
s: ?m.45141
s 
r: ?m.45144
r (
x: ?m.45147
x : 
M: Type v
M)
#align sub_mul_action.is_scalar_tower' 
SubMulAction.isScalarTower': βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) {S' : Type u_1} [inst_5 : SMul S' R]
  [inst_6 : SMul S' S] [inst_7 : SMul S' M] [inst_8 : IsScalarTower S' R M] [inst_9 : IsScalarTower S' S M],
  IsScalarTower S' S { x // x ∈ p }
SubMulAction.isScalarTower'

@[simp, norm_cast]
theorem 
val_smul_of_tower: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : { x // x ∈ p }),
  ↑(s β€’ x) = s β€’ ↑x
val_smul_of_tower (
s: S
s : 
S: Type u'
S) (
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : ((
s: S
s β€’ 
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : 
M: Type v
M) = 
s: S
s β€’ (
x: { x // x ∈ p }
x : 
M: Type v
M) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.47137} {a : Ξ±}, a = a
rfl
#align sub_mul_action.coe_smul_of_tower 
SubMulAction.val_smul_of_tower: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : { x // x ∈ p }),
  ↑(s β€’ x) = s β€’ ↑x
SubMulAction.val_smul_of_tower

@[simp]
theorem 
smul_mem_iff': βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M) {G : Type u_1}
  [inst_2 : Group G] [inst_3 : SMul G R] [inst_4 : MulAction G M] [inst_5 : IsScalarTower G R M] (g : G) {x : M},
  g β€’ x ∈ p ↔ x ∈ p
smul_mem_iff' {
G: Type u_1
G} [
Group: Type ?u.48655 β†’ Type ?u.48655
Group 
G: ?m.48652
G] [
SMul: Type ?u.48659 β†’ Type ?u.48658 β†’ Type (max?u.48659?u.48658)
SMul 
G: ?m.48652
G 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.48663) β†’ Type ?u.48662 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.48663?u.48662)
MulAction 
G: ?m.48652
G 
M: Type v
M] [
IsScalarTower: (M : Type ?u.48953) β†’
  (N : Type ?u.48952) β†’ (Ξ± : Type ?u.48951) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
G: ?m.48652
G 
R: Type u
R 
M: Type v
M] (
g: G
g : 
G: ?m.48652
G)
    {
x: M
x : 
M: Type v
M} : 
g: G
g β€’ 
x: M
x ∈ 
p: SubMulAction R M
p ↔ 
x: M
x ∈ 
p: SubMulAction R M
p :=
  ⟨fun 
h: ?m.51298
h => 
inv_smul_smul: βˆ€ {Ξ± : Type ?u.51301} {Ξ² : Type ?u.51300} [inst : Group Ξ±] [inst_1 : MulAction Ξ± Ξ²] (c : Ξ±) (x : Ξ²), c⁻¹ β€’ c β€’ x = x
inv_smul_smul 
g: G
g 
x: M
x β–Έ 
p: SubMulAction R M
p.
smul_of_tower_mem: βˆ€ {S : Type ?u.51321} {R : Type ?u.51322} {M : Type ?u.51320} [inst : Monoid R] [inst_1 : MulAction R M]
  [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M},
  x ∈ p β†’ s β€’ x ∈ p
smul_of_tower_mem 
g: G
g⁻¹ 
h: ?m.51298
h, 
p: SubMulAction R M
p.
smul_of_tower_mem: βˆ€ {S : Type ?u.52387} {R : Type ?u.52388} {M : Type ?u.52386} [inst : Monoid R] [inst_1 : MulAction R M]
  [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M},
  x ∈ p β†’ s β€’ x ∈ p
smul_of_tower_mem 
g: G
g⟩
#align sub_mul_action.smul_mem_iff' 
SubMulAction.smul_mem_iff': βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M) {G : Type u_1}
  [inst_2 : Group G] [inst_3 : SMul G R] [inst_4 : MulAction G M] [inst_5 : IsScalarTower G R M] (g : G) {x : M},
  g β€’ x ∈ p ↔ x ∈ p
SubMulAction.smul_mem_iff'

instance 
isCentralScalar: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) [inst_5 : SMul Sᡐᡒᡖ R]
  [inst_6 : SMul Sᡐᡒᡖ M] [inst_7 : IsScalarTower Sᡐᡒᡖ R M] [inst_8 : IsCentralScalar S M],
  IsCentralScalar S { x // x ∈ p }
isCentralScalar [
SMul: Type ?u.53809 β†’ Type ?u.53808 β†’ Type (max?u.53809?u.53808)
SMul 
S: Type u'
Sᡐᡒᡖ 
R: Type u
R] [
SMul: Type ?u.53814 β†’ Type ?u.53813 β†’ Type (max?u.53814?u.53813)
SMul 
S: Type u'
Sᡐᡒᡖ 
M: Type v
M] [
IsScalarTower: (M : Type ?u.53820) β†’
  (N : Type ?u.53819) β†’ (Ξ± : Type ?u.53818) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S: Type u'
Sᡐᡒᡖ 
R: Type u
R 
M: Type v
M]
    [
IsCentralScalar: (M : Type ?u.54554) β†’ (Ξ± : Type ?u.54553) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul Mᡐᡒᡖ Ξ±] β†’ Prop
IsCentralScalar 
S: Type u'
S 
M: Type v
M] :
    
IsCentralScalar: (M : Type ?u.54573) β†’ (Ξ± : Type ?u.54572) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul Mᡐᡒᡖ Ξ±] β†’ Prop
IsCentralScalar 
S: Type u'
S 
p: SubMulAction R M
p where
  op_smul_eq_smul 
r: ?m.54995
r 
x: ?m.54998
x := 
Subtype.ext: βˆ€ {Ξ± : Sort ?u.55000} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 β†’ a1 = a2
Subtype.ext <| 
op_smul_eq_smul: βˆ€ {M : Type ?u.55015} {Ξ± : Type ?u.55014} [inst : SMul M Ξ±] [inst_1 : SMul Mᡐᡒᡖ Ξ±] [self : IsCentralScalar M Ξ±] (m : M)
  (a : Ξ±), MulOpposite.op m β€’ a = m β€’ a
op_smul_eq_smul 
r: ?m.54995
r (
x: ?m.54998
x : 
M: Type v
M)

end

section

variable [
Monoid: Type ?u.58488 β†’ Type ?u.58488
Monoid 
S: Type u'
S] [
SMul: Type ?u.58492 β†’ Type ?u.58491 β†’ Type (max?u.58492?u.58491)
SMul 
S: Type u'
S 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.55285) β†’ Type ?u.55284 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.55285?u.55284)
MulAction 
S: Type u'
S 
M: Type v
M] [
IsScalarTower: (M : Type ?u.56627) β†’
  (N : Type ?u.56626) β†’ (Ξ± : Type ?u.56625) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S: Type u'
S 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.59793) β†’ (M : Type ?u.59792) β†’ [inst : SMul R M] β†’ Type ?u.59792
SubMulAction 
R: Type u
R 
M: Type v
M)

/-- If the scalar product forms a `MulAction`, then the subset inherits this action -/
instance 
mulAction': MulAction S { x // x ∈ p }
mulAction' : 
MulAction: (Ξ± : Type ?u.60348) β†’ Type ?u.60347 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.60348?u.60347)
MulAction 
S: Type u'
S 
p: SubMulAction R M
p where
  smul := 
(Β· β€’ Β·): S β†’ { x // x ∈ p } β†’ { x // x ∈ p }
(Β· β€’ Β·)
  one_smul 
x: ?m.61352
x := 
Subtype.ext: βˆ€ {Ξ± : Sort ?u.61354} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 β†’ a1 = a2
Subtype.ext <| 
one_smul: βˆ€ (M : Type ?u.61368) {Ξ± : Type ?u.61367} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β€’ b = b
one_smul 
_: Type ?u.61368
_ (
x: ?m.61352
x : 
M: Type v
M)
  mul_smul 
c₁: ?m.61545
c₁ 
cβ‚‚: ?m.61548
cβ‚‚ 
x: ?m.61551
x := 
Subtype.ext: βˆ€ {Ξ± : Sort ?u.61553} {p : Ξ± β†’ Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 β†’ a1 = a2
Subtype.ext <| 
mul_smul: βˆ€ {Ξ± : Type ?u.61564} {Ξ² : Type ?u.61563} [inst : Monoid Ξ±] [self : MulAction Ξ± Ξ²] (x y : Ξ±) (b : Ξ²),
  (x * y) β€’ b = x β€’ y β€’ b
mul_smul 
c₁: ?m.61545
c₁ 
cβ‚‚: ?m.61548
cβ‚‚ (
x: ?m.61551
x : 
M: Type v
M)
#align sub_mul_action.mul_action' 
SubMulAction.mulAction': {S : Type u'} β†’
  {R : Type u} β†’
    {M : Type v} β†’
      [inst : Monoid R] β†’
        [inst_1 : MulAction R M] β†’
          [inst_2 : Monoid S] β†’
            [inst_3 : SMul S R] β†’
              [inst_4 : MulAction S M] β†’
                [inst_5 : IsScalarTower S R M] β†’ (p : SubMulAction R M) β†’ MulAction S { x // x ∈ p }
SubMulAction.mulAction'

instance 
mulAction: MulAction R { x // x ∈ p }
mulAction : 
MulAction: (Ξ± : Type ?u.63716) β†’ Type ?u.63715 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.63716?u.63715)
MulAction 
R: Type u
R 
p: SubMulAction R M
p :=
  
p: SubMulAction R M
p.
mulAction': {S : Type ?u.63883} β†’
  {R : Type ?u.63884} β†’
    {M : Type ?u.63882} β†’
      [inst : Monoid R] β†’
        [inst_1 : MulAction R M] β†’
          [inst_2 : Monoid S] β†’
            [inst_3 : SMul S R] β†’
              [inst_4 : MulAction S M] β†’
                [inst_5 : IsScalarTower S R M] β†’ (p : SubMulAction R M) β†’ MulAction S { x // x ∈ p }
mulAction'
#align sub_mul_action.mul_action 
SubMulAction.mulAction: {R : Type u} β†’
  {M : Type v} β†’ [inst : Monoid R] β†’ [inst_1 : MulAction R M] β†’ (p : SubMulAction R M) β†’ MulAction R { x // x ∈ p }
SubMulAction.mulAction

end

/-- Orbits in a `SubMulAction` coincide with orbits in the ambient space. -/
theorem 
val_image_orbit: βˆ€ {p : SubMulAction R M} (m : { x // x ∈ p }), Subtype.val '' MulAction.orbit R m = MulAction.orbit R ↑m
val_image_orbit {
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.65229) β†’ (M : Type ?u.65228) β†’ [inst : SMul R M] β†’ Type ?u.65228
SubMulAction 
R: Type u
R 
M: Type v
M} (
m: { x // x ∈ p }
m : 
p: SubMulAction R M
p) :
    
Subtype.val: {Ξ± : Sort ?u.65975} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
Subtype.val '' 
MulAction.orbit: (Ξ± : Type ?u.65985) β†’ {Ξ² : Type ?u.65984} β†’ [inst : Monoid Ξ±] β†’ [inst : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Set Ξ²
MulAction.orbit 
R: Type u
R 
m: { x // x ∈ p }
m = 
MulAction.orbit: (Ξ± : Type ?u.66083) β†’ {Ξ² : Type ?u.66082} β†’ [inst : Monoid Ξ±] β†’ [inst : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Set Ξ²
MulAction.orbit 
R: Type u
R (
m: { x // x ∈ p }
m : 
M: Type v
M) :=
  (
Set.range_comp: βˆ€ {Ξ± : Type ?u.66201} {Ξ² : Type ?u.66199} {ΞΉ : Sort ?u.66200} (g : Ξ± β†’ Ξ²) (f : ΞΉ β†’ Ξ±),
  Set.range (g ∘ f) = g '' Set.range f
Set.range_comp 
_: ?m.66202 β†’ ?m.66203
_ 
_: ?m.66204 β†’ ?m.66202
_).
symm: βˆ€ {Ξ± : Sort ?u.66207} {a b : Ξ±}, a = b β†’ b = a
symm
#align sub_mul_action.coe_image_orbit 
SubMulAction.val_image_orbit: βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : { x // x ∈ p }),
  Subtype.val '' MulAction.orbit R m = MulAction.orbit R ↑m
SubMulAction.val_image_orbit

/- -- Previously, the relatively useless :
lemma orbit_of_sub_mul {p : SubMulAction R M} (m : p) :
  (mul_action.orbit R m : set M) = MulAction.orbit R (m : M) := rfl
-/
/-- Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space -/
theorem 
stabilizer_of_subMul.submonoid: βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : { x // x ∈ p }),
  MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
stabilizer_of_subMul.submonoid {
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.66278) β†’ (M : Type ?u.66277) β†’ [inst : SMul R M] β†’ Type ?u.66277
SubMulAction 
R: Type u
R 
M: Type v
M} (
m: { x // x ∈ p }
m : 
p: SubMulAction R M
p) :
    
MulAction.Stabilizer.submonoid: (Ξ± : Type ?u.67021) β†’ {Ξ² : Type ?u.67020} β†’ [inst : Monoid Ξ±] β†’ [inst_1 : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Submonoid Ξ±
MulAction.Stabilizer.submonoid 
R: Type u
R 
m: { x // x ∈ p }
m = 
MulAction.Stabilizer.submonoid: (Ξ± : Type ?u.67081) β†’ {Ξ² : Type ?u.67080} β†’ [inst : Monoid Ξ±] β†’ [inst_1 : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Submonoid Ξ±
MulAction.Stabilizer.submonoid 
R: Type u
R (
m: { x // x ∈ p }
m : 
M: Type v
M) := 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Monoid R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Monoid R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

x✝: R

h
x✝ ∈ MulAction.Stabilizer.submonoid R m ↔ x✝ ∈ MulAction.Stabilizer.submonoid R ↑m
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Monoid R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
Goals accomplished! πŸ™

#align sub_mul_action.stabilizer_of_sub_mul.submonoid 
SubMulAction.stabilizer_of_subMul.submonoid: βˆ€ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : { x // x ∈ p }),
  MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m
SubMulAction.stabilizer_of_subMul.submonoid

end MulActionMonoid

section MulActionGroup

variable [
Group: Type ?u.68990 β†’ Type ?u.68990
Group 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.68994) β†’ Type ?u.68993 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.68994?u.68993)
MulAction 
R: Type u
R 
M: Type v
M]

/-- Stabilizers in group SubMulAction coincide with stabilizers in the ambient space -/
theorem 
stabilizer_of_subMul: βˆ€ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : { x // x ∈ p }),
  MulAction.stabilizer R m = MulAction.stabilizer R ↑m
stabilizer_of_subMul {
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.69284) β†’ (M : Type ?u.69283) β†’ [inst : SMul R M] β†’ Type ?u.69283
SubMulAction 
R: Type u
R 
M: Type v
M} (
m: { x // x ∈ p }
m : 
p: SubMulAction R M
p) :
    
MulAction.stabilizer: (Ξ± : Type ?u.70303) β†’ {Ξ² : Type ?u.70302} β†’ [inst : Group Ξ±] β†’ [inst_1 : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Subgroup Ξ±
MulAction.stabilizer 
R: Type u
R 
m: { x // x ∈ p }
m = 
MulAction.stabilizer: (Ξ± : Type ?u.70581) β†’ {Ξ² : Type ?u.70580} β†’ [inst : Group Ξ±] β†’ [inst_1 : MulAction Ξ± Ξ²] β†’ Ξ² β†’ Subgroup Ξ±
MulAction.stabilizer 
R: Type u
R (
m: { x // x ∈ p }
m : 
M: Type v
M) := 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Group R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

MulAction.stabilizer R m = MulAction.stabilizer R ↑m
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Group R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

MulAction.stabilizer R m = MulAction.stabilizer R ↑m
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Group R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

(MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Group R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

(MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝¹: Group R

inst✝: MulAction R M

p: SubMulAction R M

m: { x // x ∈ p }

MulAction.stabilizer R m = MulAction.stabilizer R ↑m
Goals accomplished! πŸ™

#align sub_mul_action.stabilizer_of_sub_mul 
SubMulAction.stabilizer_of_subMul: βˆ€ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : { x // x ∈ p }),
  MulAction.stabilizer R m = MulAction.stabilizer R ↑m
SubMulAction.stabilizer_of_subMul

end MulActionGroup

section Module

variable [
Semiring: Type ?u.70828 β†’ Type ?u.70828
Semiring 
R: Type u
R] [
AddCommMonoid: Type ?u.70831 β†’ Type ?u.70831
AddCommMonoid 
M: Type v
M]

variable [
Module: (R : Type ?u.70889) β†’
  (M : Type ?u.70888) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.70889?u.70888)
Module 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.71787) β†’ (M : Type ?u.71786) β†’ [inst : SMul R M] β†’ Type ?u.71786
SubMulAction 
R: Type u
R 
M: Type v
M)

theorem 
zero_mem: Set.Nonempty ↑p β†’ 0 ∈ p
zero_mem (
h: Set.Nonempty ↑p
h : (
p: SubMulAction R M
p : 
Set: Type ?u.72619 β†’ Type ?u.72619
Set 
M: Type v
M).
Nonempty: {Ξ± : Type ?u.72726} β†’ Set Ξ± β†’ Prop
Nonempty) : (
0: ?m.72753
0 : 
M: Type v
M) ∈ 
p: SubMulAction R M
p :=
  let ⟨
x: M
x, 
hx: x ∈ ↑p
hx⟩ := 
h: Set.Nonempty ↑p
h
  
zero_smul: βˆ€ (R : Type ?u.73380) {M : Type ?u.73379} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M),
  0 β€’ m = 0
zero_smul 
R: Type u
R (
x: M
x : 
M: Type v
M) β–Έ 
p: SubMulAction R M
p.
smul_mem: βˆ€ {R : Type ?u.74064} {M : Type ?u.74063} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x ∈ p β†’ r β€’ x ∈ p
smul_mem 
0: ?m.74077
0 
hx: x ∈ ↑p
hx
#align sub_mul_action.zero_mem 
SubMulAction.zero_mem: βˆ€ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : SubMulAction R M),
  Set.Nonempty ↑p β†’ 0 ∈ p
SubMulAction.zero_mem

/-- If the scalar product forms a `Module`, and the `SubMulAction` is not `βŠ₯`, then the
subset inherits the zero. -/

instance: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Semiring R] β†’
      [inst_1 : AddCommMonoid M] β†’
        [inst_2 : Module R M] β†’ (p : SubMulAction R M) β†’ [n_empty : Nonempty { x // x ∈ p }] β†’ Zero { x // x ∈ p }
instance [
n_empty: Nonempty { x // x ∈ p }
n_empty : 
Nonempty: Sort ?u.75799 β†’ Prop
Nonempty 
p: SubMulAction R M
p] : 
Zero: Type ?u.75981 β†’ Type ?u.75981
Zero 
p: SubMulAction R M
p where
  zero := ⟨
0: ?m.76136
0, 
n_empty: Nonempty { x // x ∈ p }
n_empty.
elim: βˆ€ {Ξ± : Sort ?u.76713} {p : Prop}, Nonempty Ξ± β†’ (Ξ± β†’ p) β†’ p
elim fun 
x: ?m.76722
x => 
p: SubMulAction R M
p.
zero_mem: βˆ€ {R : Type ?u.76725} {M : Type ?u.76724} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : SubMulAction R M), Set.Nonempty ↑p β†’ 0 ∈ p
zero_mem ⟨
x: ?m.76722
x, 
x: ?m.76722
x.
prop: βˆ€ {Ξ± : Sort ?u.76921} {p : Ξ± β†’ Prop} (x : Subtype p), p ↑x
prop⟩⟩

end Module

section AddCommGroup

variable [
Ring: Type ?u.77079 β†’ Type ?u.77079
Ring 
R: Type u
R] [
AddCommGroup: Type ?u.77082 β†’ Type ?u.77082
AddCommGroup 
M: Type v
M]

variable [
Module: (R : Type ?u.80931) β†’
  (M : Type ?u.80930) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.80931?u.80930)
Module 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p 
p': SubMulAction R M
p' : 
SubMulAction: (R : Type ?u.79277) β†’ (M : Type ?u.79276) β†’ [inst : SMul R M] β†’ Type ?u.79276
SubMulAction 
R: Type u
R 
M: Type v
M)

variable {
r: R
r : 
R: Type u
R} {
x: M
x 
y: M
y : 
M: Type v
M}

theorem 
neg_mem: x ∈ p β†’ -x ∈ p
neg_mem (
hx: x ∈ p
hx : 
x: M
x ∈ 
p: SubMulAction R M
p) : -
x: M
x ∈ 
p: SubMulAction R M
p := 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

hx: x ∈ p

-x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

hx: x ∈ p

-x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

hx: x ∈ p

-1 β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

hx: x ∈ p

-1 β€’ x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

hx: x ∈ p

-x ∈ p
Goals accomplished! πŸ™

#align sub_mul_action.neg_mem 
SubMulAction.neg_mem: βˆ€ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  {x : M}, x ∈ p β†’ -x ∈ p
SubMulAction.neg_mem

@[simp]
theorem 
neg_mem_iff: -x ∈ p ↔ x ∈ p
neg_mem_iff : -
x: M
x ∈ 
p: SubMulAction R M
p ↔ 
x: M
x ∈ 
p: SubMulAction R M
p :=
  ⟨fun 
h: ?m.85870
h => 
Goals accomplished! πŸ™
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

h: -x ∈ p

x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

h: -x ∈ p

x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

h: -x ∈ p

- -x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

h: -x ∈ p

- -x ∈ p
S: Type u'

T: Type u''

R: Type u

M: Type v

inst✝²: Ring R

inst✝¹: AddCommGroup M

inst✝: Module R M

p, p': SubMulAction R M

r: R

x, y: M

h: -x ∈ p

x ∈ p
Goals accomplished! πŸ™
, 
neg_mem: βˆ€ {R : Type ?u.85877} {M : Type ?u.85876} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : SubMulAction R M) {x : M}, x ∈ p β†’ -x ∈ p
neg_mem 
_: SubMulAction ?m.85878 ?m.85879
_⟩
#align sub_mul_action.neg_mem_iff 
SubMulAction.neg_mem_iff: βˆ€ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  {x : M}, -x ∈ p ↔ x ∈ p
SubMulAction.neg_mem_iff


instance: {R : Type u} β†’
  {M : Type v} β†’
    [inst : Ring R] β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (p : SubMulAction R M) β†’ Neg { x // x ∈ p }
instance : 
Neg: Type ?u.88383 β†’ Type ?u.88383
Neg 
p: SubMulAction R M
p :=
  ⟨fun 
x: ?m.88552
x => ⟨-
x: ?m.88552
x.
1: {Ξ± : Sort ?u.88567} β†’ {p : Ξ± β†’ Prop} β†’ Subtype p β†’ Ξ±
1, 
neg_mem: βˆ€ {R : Type ?u.88710} {M : Type ?u.88709} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : SubMulAction R M) {x : M}, x ∈ p β†’ -x ∈ p
neg_mem 
_: SubMulAction ?m.88711 ?m.88712
_ 
x: ?m.88552
x.
2: βˆ€ {Ξ± : Sort ?u.88837} {p : Ξ± β†’ Prop} (self : Subtype p), p ↑self
2⟩⟩

@[simp, norm_cast]
theorem 
val_neg: βˆ€ (x : { x // x ∈ p }), ↑(-x) = -↑x
val_neg (
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : ((-
x: { x // x ∈ p }
x : 
p: SubMulAction R M
p) : 
M: Type v
M) = -
x: { x // x ∈ p }
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.91230} {a : Ξ±}, a = a
rfl
#align sub_mul_action.coe_neg 
SubMulAction.val_neg: βˆ€ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : SubMulAction R M)
  (x : { x // x ∈ p }), ↑(-x) = -↑x
SubMulAction.val_neg

end AddCommGroup

end SubMulAction

namespace SubMulAction

variable [
GroupWithZero: Type ?u.95321 β†’ Type ?u.95321
GroupWithZero 
S: Type u'
S] [
Monoid: Type ?u.93077 β†’ Type ?u.93077
Monoid 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.91395) β†’ Type ?u.91394 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.91395?u.91394)
MulAction 
R: Type u
R 
M: Type v
M]

variable [
SMul: Type ?u.93094 β†’ Type ?u.93093 β†’ Type (max?u.93094?u.93093)
SMul 
S: Type u'
S 
R: Type u
R] [
MulAction: (Ξ± : Type ?u.95345) β†’ Type ?u.95344 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.95345?u.95344)
MulAction 
S: Type u'
S 
M: Type v
M] [
IsScalarTower: (M : Type ?u.91629) β†’
  (N : Type ?u.91628) β†’ (Ξ± : Type ?u.91627) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower 
S: Type u'
S 
R: Type u
R 
M: Type v
M]

variable (
p: SubMulAction R M
p : 
SubMulAction: (R : Type ?u.97000) β†’ (M : Type ?u.96999) β†’ [inst : SMul R M] β†’ Type ?u.96999
SubMulAction 
R: Type u
R 
M: Type v
M) {
s: S
s : 
S: Type u'
S} {
x: M
x 
y: M
y : 
M: Type v
M}

theorem 
smul_mem_iff: s β‰  0 β†’ (s β€’ x ∈ p ↔ x ∈ p)
smul_mem_iff (
s0: s β‰  0
s0 : 
s: S
s β‰  
0: ?m.97563
0) : 
s: S
s β€’ 
x: M
x ∈ 
p: SubMulAction R M
p ↔ 
x: M
x ∈ 
p: SubMulAction R M
p :=
  
p: SubMulAction R M
p.
smul_mem_iff': βˆ€ {R : Type ?u.98760} {M : Type ?u.98759} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M)
  {G : Type ?u.98761} [inst_2 : Group G] [inst_3 : SMul G R] [inst_4 : MulAction G M] [inst_5 : IsScalarTower G R M]
  (g : G) {x : M}, g β€’ x ∈ p ↔ x ∈ p
smul_mem_iff' (
Units.mk0: {Gβ‚€ : Type ?u.98805} β†’ [inst : GroupWithZero Gβ‚€] β†’ (a : Gβ‚€) β†’ a β‰  0 β†’ Gβ‚€Λ£
Units.mk0 
s: S
s 
s0: s β‰  0
s0)
#align sub_mul_action.smul_mem_iff 
SubMulAction.smul_mem_iff: βˆ€ {S : Type u'} {R : Type u} {M : Type v} [inst : GroupWithZero S] [inst_1 : Monoid R] [inst_2 : MulAction R M]
  [inst_3 : SMul S R] [inst_4 : MulAction S M] [inst_5 : IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M},
  s β‰  0 β†’ (s β€’ x ∈ p ↔ x ∈ p)
SubMulAction.smul_mem_iff

end SubMulAction