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.
```/-
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 uR : Type u: Type (u+1)Type u} {M: Type vM : 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 SMulMemClass: (S : Type u_1) β (R : outParam (Type u_2)) β (M : Type u_3) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass (S: Type ?u.18S : Type _: Type (?u.18+1)Type _) (R: outParam (Type ?u.22)R : outParam: Sort ?u.21 β Sort ?u.21outParam <| Type _: Type (?u.22+1)Type _) (M: Type ?u.25M : 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.25M] [SetLike: Type ?u.33 β outParam (Type ?u.32) β Type (max?u.33?u.32)SetLike S: Type ?u.18S M: Type ?u.25M] 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 β ssmul_mem : β {s: Ss : S: Type ?u.18S} (r: Rr : R: outParam (Type ?u.22)R) {m: Mm : M: Type ?u.25M}, m: Mm β s: Ss β r: Rr β’ m: Mm β s: Ss
#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] β TypeSMulMemClass

/-- `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 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 MVAddMemClass (S: Type ?u.163S : Type _: Type (?u.163+1)Type _) (R: outParam (Type ?u.167)R : outParam: Sort ?u.166 β Sort ?u.166outParam <| Type _: Type (?u.167+1)Type _) (M: Type ?u.170M : 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.170M] [SetLike: Type ?u.178 β outParam (Type ?u.177) β Type (max?u.178?u.177)SetLike S: Type ?u.163S M: Type ?u.170M] 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 β svadd_mem : β {s: Ss : S: Type ?u.163S} (r: Rr : R: outParam (Type ?u.167)R) {m: Mm : M: Type ?u.170M}, m: Mm β s: Ss β r: Rr +α΅₯ m: Mm β s: Ss
#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] β TypeVAddMemClass

attribute [to_additive: (S : Type u_1) β (R : outParam (Type u_2)) β (M : Type u_3) β [inst : VAdd R M] β [inst : SetLike S M] β Typeto_additive] SMulMemClass: (S : Type u_1) β (R : outParam (Type u_2)) β (M : Type u_3) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass

namespace SetLike

variable [SMul: Type ?u.1093 β Type ?u.1092 β Type (max?u.1093?u.1092)SMul R: Type uR M: Type vM] [SetLike: Type ?u.1097 β outParam (Type ?u.1096) β Type (max?u.1097?u.1096)SetLike S: Type u'S M: Type vM] [hS: SMulMemClass S R MhS : SMulMemClass: (S : Type ?u.321) β (R : outParam (Type ?u.320)) β (M : Type ?u.319) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass S: Type u'S R: Type uR M: Type vM] (s: Ss : 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 uR s: Ss :=
β¨fun r: ?m.535r x: ?m.538x => β¨r: ?m.535r β’ x: ?m.538x.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 β ssmul_mem r: ?m.535r x: ?m.538x.2: β {Ξ± : Sort ?u.658} {p : Ξ± β Prop} (self : Subtype p), p βself2β©β©
#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
{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 +α΅₯ βxto_additive (attr := simp, norm_cast)]
protected theorem val_smul: β (r : R) (x : { x // x β s }), β(r β’ x) = r β’ βxval_smul (r: Rr : R: Type uR) (x: { x // x β s }x : s: Ss) : (β(r: Rr β’ x: { x // x β s }x) : M: Type vM) = r: Rr β’ (x: { x // x β s }x : M: Type vM) :=
rfl: β {Ξ± : Sort ?u.3246} {a : Ξ±}, a = arfl
#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 β’ βxSetLike.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 +α΅₯ βxSetLike.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: Rr : R: Type uR) (x: Mx : M: Type vM) (hx: x β shx : x: Mx β s: Ss) : r: Rr β’ (β¨x: Mx, hx: x β shxβ© : s: Ss) = β¨r: Rr β’ x: Mx, 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 β ssmul_mem r: Rr hx: x β shxβ© :=
rfl: β {Ξ± : Sort ?u.5764} {a : Ξ±}, a = arfl
#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: Rr : R: Type uR) (x: { x // x β s }x : s: Ss) : r: Rr β’ x: { x // x β s }x = β¨r: Rr β’ 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 β ssmul_mem r: Rr x: { x // x β s }x.2: β {Ξ± : Sort ?u.9667} {p : Ξ± β Prop} (self : Subtype p), p βself2β© :=
rfl: β {Ξ± : Sort ?u.9691} {a : Ξ±}, a = arfl
#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 β Nforall_smul_mem_iff {R: Type u_1R M: Type ?u.9796M S: Type ?u.9799S : Type _: Type (?u.9793+1)Type _} [Monoid: Type ?u.9802 β Type ?u.9802Monoid R: Type ?u.9793R] [MulAction: (Ξ± : Type ?u.9806) β Type ?u.9805 β [inst : Monoid Ξ±] β Type (max?u.9806?u.9805)MulAction R: Type ?u.9793R M: Type ?u.9796M] [SetLike: Type ?u.9819 β outParam (Type ?u.9818) β Type (max?u.9819?u.9818)SetLike S: Type ?u.9799S M: Type ?u.9796M]
[SMulMemClass: (S : Type ?u.9824) β
(R : outParam (Type ?u.9823)) β (M : Type ?u.9822) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass S: Type ?u.9799S R: Type ?u.9793R M: Type ?u.9796M] {N: SN : S: Type ?u.9799S} {x: Mx : M: Type ?u.9796M} : (β a: Ra : R: Type ?u.9793R, a: Ra β’ x: Mx β N: SN) β x: Mx β N: SN :=
β¨fun h: ?m.11175h => byGoals accomplished! π Sβ: Type u'T: Type u''Rβ: Type uMβ: Type vinstββ΅: SMul Rβ Mβinstββ΄: SetLike Sβ MβhS: SMulMemClass Sβ Rβ Mβs: SβR: Type u_1M: Type u_2S: Type u_3instβΒ³: Monoid RinstβΒ²: MulAction R MinstβΒΉ: SetLike S Minstβ: SMulMemClass S R MN: Sx: Mh: β (a : R), a β’ x β Nx β Nsimpa using h: β (a : R), a β’ x β Nh 1: ?m.120151Goals accomplished! π, fun h: ?m.11185h a: ?m.11188a => 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 β sSMulMemClass.smul_mem a: ?m.11188a h: ?m.11185hβ©
#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 β NSetLike.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 MSubMulAction (R: Type uR : Type u: Type (u+1)Type u) (M: Type vM : Type v: Type (v+1)Type v) [SMul: Type ?u.12566 β Type ?u.12565 β Type (max?u.12566?u.12565)SMul R: Type uR M: Type vM] : 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 Mcarrier : Set: Type ?u.12570 β Type ?u.12570Set M: Type vM
/-- 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.carriersmul_mem' : β (c: Rc : R: Type uR) {x: Mx : M: Type vM}, x: Mx β carrier: Set Mcarrier β c: Rc β’ x: Mx β carrier: Set Mcarrier
#align sub_mul_action SubMulAction: (R : Type u) β (M : Type v) β [inst : SMul R M] β Type vSubMulAction

namespace SubMulAction

variable [SMul: Type ?u.13591 β Type ?u.13590 β Type (max?u.13591?u.13590)SMul R: Type uR M: Type vM]

instance: {R : Type u} β {M : Type v} β [inst : SMul R M] β SetLike (SubMulAction R M) Minstance : 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.13099SubMulAction R: Type uR M: Type vM) M: Type vM :=
β¨SubMulAction.carrier: {R : Type ?u.13125} β {M : Type ?u.13124} β [inst : SMul R M] β SubMulAction R M β Set MSubMulAction.carrier, fun p: ?m.13187p q: ?m.13190q h: ?m.13193h => byGoals accomplished! π S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp, q: SubMulAction R Mh: p.carrier = q.carrierp = qcases p: SubMulAction R MpS: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mq: SubMulAction R Mcarrierβ: Set Msmul_mem'β: β (c : R) {x : M}, x β carrierβ β c β’ x β carrierβh: { carrier := carrierβ, smul_mem' := smul_mem'β }.carrier = q.carriermk{ carrier := carrierβ, smul_mem' := smul_mem'β } = q;S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mq: SubMulAction R Mcarrierβ: Set Msmul_mem'β: β (c : R) {x : M}, x β carrierβ β c β’ x β carrierβh: { carrier := carrierβ, smul_mem' := smul_mem'β }.carrier = q.carriermk{ carrier := carrierβ, smul_mem' := smul_mem'β } = q S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp, q: SubMulAction R Mh: p.carrier = q.carrierp = qcases q: SubMulAction R MqS: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R McarrierβΒΉ: Set Msmul_mem'βΒΉ: β (c : R) {x : M}, x β carrierβΒΉ β c β’ x β carrierβΒΉcarrierβ: Set Msmul_mem'β: β (c : R) {x : M}, x β carrierβ β c β’ x β carrierβh: { carrier := carrierβΒΉ, smul_mem' := smul_mem'βΒΉ }.carrier = { carrier := carrierβ, smul_mem' := smul_mem'β }.carriermk.mk{ carrier := carrierβΒΉ, smul_mem' := smul_mem'βΒΉ } = { carrier := carrierβ, smul_mem' := smul_mem'β };S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R McarrierβΒΉ: Set Msmul_mem'βΒΉ: β (c : R) {x : M}, x β carrierβΒΉ β c β’ x β carrierβΒΉcarrierβ: Set Msmul_mem'β: β (c : R) {x : M}, x β carrierβ β c β’ x β carrierβh: { carrier := carrierβΒΉ, smul_mem' := smul_mem'βΒΉ }.carrier = { carrier := carrierβ, smul_mem' := smul_mem'β }.carriermk.mk{ carrier := carrierβΒΉ, smul_mem' := smul_mem'βΒΉ } = { carrier := carrierβ, smul_mem' := smul_mem'β } S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp, q: SubMulAction R Mh: p.carrier = q.carrierp = qcongrGoals accomplished! π β©

instance: {R : Type u} β {M : Type v} β [inst : SMul R M] β SMulMemClass (SubMulAction R M) R Minstance : SMulMemClass: (S : Type ?u.13596) β
(R : outParam (Type ?u.13595)) β (M : Type ?u.13594) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass (SubMulAction: (R : Type ?u.13598) β (M : Type ?u.13597) β [inst : SMul R M] β Type ?u.13597SubMulAction R: Type uR M: Type vM) R: Type uR M: Type vM 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.carriersmul_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 β βpmem_carrier {p: SubMulAction R Mp : SubMulAction: (R : Type ?u.13808) β (M : Type ?u.13807) β [inst : SMul R M] β Type ?u.13807SubMulAction R: Type uR M: Type vM} {x: Mx : M: Type vM} : x: Mx β p: SubMulAction R Mp.carrier: {R : Type ?u.13830} β {M : Type ?u.13829} β [inst : SMul R M] β SubMulAction R M β Set Mcarrier β x: Mx β (p: SubMulAction R Mp : Set: Type ?u.13856 β Type ?u.13856Set M: Type vM) :=
Iff.rfl: β {a : Prop}, a β aIff.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 β βpSubMulAction.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 = qext {p: SubMulAction R Mp q: SubMulAction R Mq : SubMulAction: (R : Type ?u.14021) β (M : Type ?u.14020) β [inst : SMul R M] β Type ?u.14020SubMulAction R: Type uR M: Type vM} (h: β (x : M), x β p β x β qh : β x: ?m.14026x, x: ?m.14026x β p: SubMulAction R Mp β x: ?m.14026x β q: SubMulAction R Mq) : p: SubMulAction R Mp = q: SubMulAction R Mq :=
SetLike.ext: β {A : Type ?u.14096} {B : Type ?u.14095} [i : SetLike A B] {p q : A}, (β (x : B), x β p β x β q) β p = qSetLike.ext h: β (x : M), x β p β x β qh
#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 = qSubMulAction.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 Mcopy (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.14169) β (M : Type ?u.14168) β [inst : SMul R M] β Type ?u.14168SubMulAction R: Type uR M: Type vM) (s: Set Ms : Set: Type ?u.14183 β Type ?u.14183Set M: Type vM) (hs: s = βphs : s: Set Ms = βp: SubMulAction R Mp) : SubMulAction: (R : Type ?u.14293) β (M : Type ?u.14292) β [inst : SMul R M] β Type ?u.14292SubMulAction R: Type uR M: Type vM
where
carrier := s: Set Ms
smul_mem' := hs: s = βphs.symm: β {Ξ± : Sort ?u.14306} {a b : Ξ±}, a = b β b = asymm βΈ p: SubMulAction R Mp.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.carriersmul_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 MSubMulAction.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) = scoe_copy (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.14437) β (M : Type ?u.14436) β [inst : SMul R M] β Type ?u.14436SubMulAction R: Type uR M: Type vM) (s: Set Ms : Set: Type ?u.14451 β Type ?u.14451Set M: Type vM) (hs: s = βphs : s: Set Ms = βp: SubMulAction R Mp) : (p: SubMulAction R Mp.copy: {R : Type ?u.14564} β
{M : Type ?u.14563} β [inst : SMul R M] β (p : SubMulAction R M) β (s : Set M) β s = βp β SubMulAction R Mcopy s: Set Ms hs: s = ?m.14458hs : Set: Type ?u.14562 β Type ?u.14562Set M: Type vM) = s: Set Ms :=
rfl: β {Ξ± : Sort ?u.14653} {a : Ξ±}, a = arfl
#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) = sSubMulAction.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 = pcopy_eq (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.14702) β (M : Type ?u.14701) β [inst : SMul R M] β Type ?u.14701SubMulAction R: Type uR M: Type vM) (s: Set Ms : Set: Type ?u.14716 β Type ?u.14716Set M: Type vM) (hs: s = βphs : s: Set Ms = βp: SubMulAction R Mp) : p: SubMulAction R Mp.copy: {R : Type ?u.14827} β
{M : Type ?u.14826} β [inst : SMul R M] β (p : SubMulAction R M) β (s : Set M) β s = βp β SubMulAction R Mcopy s: Set Ms hs: s = ?m.14723hs = p: SubMulAction R Mp :=
SetLike.coe_injective: β {A : Type ?u.14847} {B : Type ?u.14848} [i : SetLike A B], Injective SetLike.coeSetLike.coe_injective hs: s = βphs
#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 = pSubMulAction.copy_eq

instance: {R : Type u} β {M : Type v} β [inst : SMul R M] β Bot (SubMulAction R M)instance : Bot: Type ?u.14908 β Type ?u.14908Bot (SubMulAction: (R : Type ?u.14910) β (M : Type ?u.14909) β [inst : SMul R M] β Type ?u.14909SubMulAction R: Type uR M: Type vM) where
bot :=
{ carrier := β: ?m.14935β
smul_mem' := fun _c: ?m.14981_c h: ?m.14984h => Set.not_mem_empty: β {Ξ± : Type ?u.14986} (x : Ξ±), Β¬x β βSet.not_mem_empty h: ?m.14984h }

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.15063SubMulAction R: Type uR M: Type vM) :=

end SubMulAction

namespace SubMulAction

section SMul

variable [SMul: Type ?u.15434 β Type ?u.15433 β Type (max?u.15434?u.15433)SMul R: Type uR M: Type vM]

variable (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.15890) β (M : Type ?u.15889) β [inst : SMul R M] β Type ?u.15889SubMulAction R: Type uR M: Type vM)

variable {r: Rr : R: Type uR} {x: Mx : M: Type vM}

theorem smul_mem: β (r : R), x β p β r β’ x β psmul_mem (r: Rr : R: Type uR) (h: x β ph : x: Mx β p: SubMulAction R Mp) : r: Rr β’ x: Mx β p: SubMulAction R Mp :=
p: SubMulAction R Mp.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.carriersmul_mem' r: Rr h: x β ph
#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 β pSubMulAction.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 uR p: SubMulAction R Mp where smul c: ?m.15617c x: ?m.15620x := β¨c: ?m.15617c β’ x: ?m.15620x.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 β psmul_mem _: SubMulAction ?m.15671 ?m.15672_ c: ?m.15617c x: ?m.15620x.2: β {Ξ± : Sort ?u.15719} {p : Ξ± β Prop} (self : Subtype p), p βself2β©

variable {p: ?m.15908p}

@[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 β’ βxval_smul (r: Rr : R: Type uR) (x: { x // x β p }x : p: SubMulAction R Mp) : (β(r: Rr β’ x: { x // x β p }x) : M: Type vM) = r: Rr β’ (x: { x // x β p }x : M: Type vM) :=
rfl: β {Ξ± : Sort ?u.16235} {a : Ξ±}, a = arfl
#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 β’ βxSubMulAction.val_smul

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

variable (p: ?m.16409p)

/-- Embedding of a submodule `p` to the ambient space `M`. -/
protected def subtype: { x // x β p } β[R] Msubtype : p: SubMulAction R Mp β[R: Type uR] M: Type vM := byGoals accomplished! π S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp: SubMulAction R Mr: Rx: M{ x // x β p } β[R] Mrefine' { toFun := Subtype.val: {Ξ± : Sort ?u.16650} β {p : Ξ± β Prop} β Subtype p β Ξ±Subtype.val.. }S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp: SubMulAction R Mr: Rx: Mβ (m : R) (x : { x // x β p }), β(m β’ x) = m β’ βx;S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp: SubMulAction R Mr: Rx: Mβ (m : R) (x : { x // x β p }), β(m β’ x) = m β’ βx S: Type u'T: Type u''R: Type uM: Type vinstβ: SMul R Mp: SubMulAction R Mr: Rx: M{ x // x β p } β[R] Msimp [val_smul: β {R : Type ?u.16663} {M : Type ?u.16662} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : { x // x β p }),
β(r β’ x) = r β’ βxval_smul]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] MSubMulAction.subtype

@[simp]
theorem subtype_apply: β (x : { x // x β p }), β(SubMulAction.subtype p) x = βxsubtype_apply (x: { x // x β p }x : p: SubMulAction R Mp) : p: SubMulAction R Mp.subtype: {R : Type ?u.20577} β {M : Type ?u.20576} β [inst : SMul R M] β (p : SubMulAction R M) β { x // x β p } β[R] Msubtype x: { x // x β p }x = x: { x // x β p }x :=
rfl: β {Ξ± : Sort ?u.20896} {a : Ξ±}, a = arfl
#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 = βxSubMulAction.subtype_apply

theorem subtype_eq_val: β(SubMulAction.subtype p) = Subtype.valsubtype_eq_val : (SubMulAction.subtype: {R : Type ?u.21012} β {M : Type ?u.21011} β [inst : SMul R M] β (p : SubMulAction R M) β { x // x β p } β[R] MSubMulAction.subtype p: SubMulAction R Mp : p: SubMulAction R Mp β M: Type vM) = Subtype.val: {Ξ± : Sort ?u.21158} β {p : Ξ± β Prop} β Subtype p β Ξ±Subtype.val :=
rfl: β {Ξ± : Sort ?u.21211} {a : Ξ±}, a = arfl
#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.valSubMulAction.subtype_eq_val

end SMul

namespace SMulMemClass

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

variable [hA: SMulMemClass A R MhA : SMulMemClass: (S : Type ?u.22041) β
(R : outParam (Type ?u.22040)) β (M : Type ?u.22039) β [inst : SMul R M] β [inst : SetLike S M] β TypeSMulMemClass A: Type ?u.21284A R: Type uR M: Type vM] (S': AS' : A: Type ?u.21284A)

-- 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 uR S': AS' :=
Subtype.coe_injective: β {Ξ± : Sort ?u.22905} {p : Ξ± β Prop}, Injective fun a => βaSubtype.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 β’ βxSetLike.val_smul S': AS')
#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] Msubtype : S': AS' β[R: Type uR] M: Type vM :=
β¨Subtype.val: {Ξ± : Sort ?u.30272} β {p : Ξ± β Prop} β Subtype p β Ξ±Subtype.val, fun _: ?m.30284_ _: ?m.30287_ => rfl: β {Ξ± : Sort ?u.30289} {a : Ξ±}, a = arflβ©
#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] MSubMulAction.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.valcoeSubtype : (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] MSMulMemClass.subtype S': AS' : S': AS' β M: Type vM) = Subtype.val: {Ξ± : Sort ?u.31432} β {p : Ξ± β Prop} β Subtype p β Ξ±Subtype.val :=
rfl: β {Ξ± : Sort ?u.31493} {a : Ξ±}, a = arfl
#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.valSubMulAction.SMulMemClass.coeSubtype

end SMulMemClass

section MulActionMonoid

variable [Monoid: Type ?u.38384 β Type ?u.38384Monoid R: Type uR] [MulAction: (Ξ± : Type ?u.42602) β Type ?u.42601 β [inst : Monoid Ξ±] β Type (max?u.42602?u.42601)MulAction R: Type uR M: Type vM]

section

variable [SMul: Type ?u.42615 β Type ?u.42614 β Type (max?u.42615?u.42614)SMul S: Type u'S R: Type uR] [SMul: Type ?u.33688 β Type ?u.33687 β Type (max?u.33688?u.33687)SMul S: Type u'S M: Type vM] [IsScalarTower: (M : Type ?u.33693) β
(N : Type ?u.33692) β (Ξ± : Type ?u.33691) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S: Type u'S R: Type uR M: Type vM]

variable (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.33105) β (M : Type ?u.33104) β [inst : SMul R M] β Type ?u.33104SubMulAction R: Type uR M: Type vM)

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 β psmul_of_tower_mem (s: Ss : S: Type u'S) {x: Mx : M: Type vM} (h: x β ph : x: Mx β p: SubMulAction R Mp) : s: Ss β’ x: Mx β p: SubMulAction R Mp := byGoals accomplished! π
S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β ps β’ x β prw [S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β ps β’ x β pβ one_smul: β (M : Type ?u.35097) {Ξ± : Type ?u.35096} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β’ b = bone_smul R: Type uR x: Mx,S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β ps β’ 1 β’ x β p S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β ps β’ x β pβ smul_assoc: β {Ξ± : Type ?u.35124} {M : Type ?u.35122} {N : Type ?u.35123} [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 β’ zsmul_assocS: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β p(s β’ 1) β’ x β p]S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β p(s β’ 1) β’ x β p
S: Type u'T: Type u''R: Type uM: Type vinstββ΄: Monoid RinstβΒ³: MulAction R MinstβΒ²: SMul S RinstβΒΉ: SMul S Minstβ: IsScalarTower S R Mp: SubMulAction R Ms: Sx: Mh: x β ps β’ x β pexact p: SubMulAction R Mp.smul_mem: β {R : Type ?u.36318} {M : Type ?u.36317} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x β p β r β’ x β psmul_mem _: ?m.36326_ h: x β phGoals 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 β pSubMulAction.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 Mp where smul c: ?m.37839c x: ?m.37842x := β¨c: ?m.37839c β’ x: ?m.37842x.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 β psmul_of_tower_mem _: SubMulAction ?m.37897 ?m.37898_ c: ?m.37839c x: ?m.37842x.2: β {Ξ± : Sort ?u.38112} {p : Ξ± β Prop} (self : Subtype p), p βself2β©
#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 Ξ±] β PropIsScalarTower S: Type u'S R: Type uR p: SubMulAction R Mp where
smul_assoc s: ?m.41808s r: ?m.41811r x: ?m.41814x := Subtype.ext: β {Ξ± : Sort ?u.41816} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.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 β’ zsmul_assoc s: ?m.41808s r: ?m.41811r (x: ?m.41814x : M: Type vM)
#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.43907S' : Type _: Type (?u.43907+1)Type _} [SMul: Type ?u.43911 β Type ?u.43910 β Type (max?u.43911?u.43910)SMul S': Type ?u.43907S' R: Type uR] [SMul: Type ?u.43915 β Type ?u.43914 β Type (max?u.43915?u.43914)SMul S': Type ?u.43907S' S: Type u'S] [SMul: Type ?u.43919 β Type ?u.43918 β Type (max?u.43919?u.43918)SMul S': Type ?u.43907S' M: Type vM] [IsScalarTower: (M : Type ?u.43924) β
(N : Type ?u.43923) β (Ξ± : Type ?u.43922) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S': Type ?u.43907S' R: Type uR M: Type vM]
[IsScalarTower: (M : Type ?u.44656) β
(N : Type ?u.44655) β (Ξ± : Type ?u.44654) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S': Type ?u.43907S' S: Type u'S M: Type vM] : IsScalarTower: (M : Type ?u.44690) β
(N : Type ?u.44689) β (Ξ± : Type ?u.44688) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S': Type ?u.43907S' S: Type u'S p: SubMulAction R Mp
where smul_assoc s: ?m.45141s r: ?m.45144r x: ?m.45147x := Subtype.ext: β {Ξ± : Sort ?u.45149} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.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 β’ zsmul_assoc s: ?m.45141s r: ?m.45144r (x: ?m.45147x : M: Type vM)
#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 β’ βxval_smul_of_tower (s: Ss : S: Type u'S) (x: { x // x β p }x : p: SubMulAction R Mp) : ((s: Ss β’ x: { x // x β p }x : p: SubMulAction R Mp) : M: Type vM) = s: Ss β’ (x: { x // x β p }x : M: Type vM) :=
rfl: β {Ξ± : Sort ?u.47137} {a : Ξ±}, a = arfl
#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 β’ βxSubMulAction.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 β psmul_mem_iff' {G: Type u_1G} [Group: Type ?u.48655 β Type ?u.48655Group G: ?m.48652G] [SMul: Type ?u.48659 β Type ?u.48658 β Type (max?u.48659?u.48658)SMul G: ?m.48652G R: Type uR] [MulAction: (Ξ± : Type ?u.48663) β Type ?u.48662 β [inst : Monoid Ξ±] β Type (max?u.48663?u.48662)MulAction G: ?m.48652G M: Type vM] [IsScalarTower: (M : Type ?u.48953) β
(N : Type ?u.48952) β (Ξ± : Type ?u.48951) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower G: ?m.48652G R: Type uR M: Type vM] (g: Gg : G: ?m.48652G)
{x: Mx : M: Type vM} : g: Gg β’ x: Mx β p: SubMulAction R Mp β x: Mx β p: SubMulAction R Mp :=
β¨fun h: ?m.51298h => inv_smul_smul: β {Ξ± : Type ?u.51301} {Ξ² : Type ?u.51300} [inst : Group Ξ±] [inst_1 : MulAction Ξ± Ξ²] (c : Ξ±) (x : Ξ²), cβ»ΒΉ β’ c β’ x = xinv_smul_smul g: Gg x: Mx βΈ p: SubMulAction R Mp.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 β psmul_of_tower_mem g: Ggβ»ΒΉ h: ?m.51298h, p: SubMulAction R Mp.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 β psmul_of_tower_mem g: Ggβ©
#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 β pSubMulAction.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 uR] [SMul: Type ?u.53814 β Type ?u.53813 β Type (max?u.53814?u.53813)SMul S: Type u'Sα΅α΅α΅ M: Type vM] [IsScalarTower: (M : Type ?u.53820) β
(N : Type ?u.53819) β (Ξ± : Type ?u.53818) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S: Type u'Sα΅α΅α΅ R: Type uR M: Type vM]
[IsCentralScalar: (M : Type ?u.54554) β (Ξ± : Type ?u.54553) β [inst : SMul M Ξ±] β [inst : SMul Mα΅α΅α΅ Ξ±] β PropIsCentralScalar S: Type u'S M: Type vM] :
IsCentralScalar: (M : Type ?u.54573) β (Ξ± : Type ?u.54572) β [inst : SMul M Ξ±] β [inst : SMul Mα΅α΅α΅ Ξ±] β PropIsCentralScalar S: Type u'S p: SubMulAction R Mp where
op_smul_eq_smul r: ?m.54995r x: ?m.54998x := Subtype.ext: β {Ξ± : Sort ?u.55000} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.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 β’ aop_smul_eq_smul r: ?m.54995r (x: ?m.54998x : M: Type vM)

end

section

variable [Monoid: Type ?u.58488 β Type ?u.58488Monoid S: Type u'S] [SMul: Type ?u.58492 β Type ?u.58491 β Type (max?u.58492?u.58491)SMul S: Type u'S R: Type uR] [MulAction: (Ξ± : Type ?u.55285) β Type ?u.55284 β [inst : Monoid Ξ±] β Type (max?u.55285?u.55284)MulAction S: Type u'S M: Type vM] [IsScalarTower: (M : Type ?u.56627) β
(N : Type ?u.56626) β (Ξ± : Type ?u.56625) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S: Type u'S R: Type uR M: Type vM]

variable (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.59793) β (M : Type ?u.59792) β [inst : SMul R M] β Type ?u.59792SubMulAction R: Type uR M: Type vM)

/-- 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 Mp where
smul := (Β· β’ Β·): S β { x // x β p } β { x // x β p }(Β· β’ Β·)
one_smul x: ?m.61352x := Subtype.ext: β {Ξ± : Sort ?u.61354} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext <| one_smul: β (M : Type ?u.61368) {Ξ± : Type ?u.61367} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β’ b = bone_smul _: Type ?u.61368_ (x: ?m.61352x : M: Type vM)
mul_smul cβ: ?m.61545cβ cβ: ?m.61548cβ x: ?m.61551x := Subtype.ext: β {Ξ± : Sort ?u.61553} {p : Ξ± β Prop} {a1 a2 : { x // p x }}, βa1 = βa2 β a1 = a2Subtype.ext <| mul_smul: β {Ξ± : Type ?u.61564} {Ξ² : Type ?u.61563} [inst : Monoid Ξ±] [self : MulAction Ξ± Ξ²] (x y : Ξ±) (b : Ξ²),
(x * y) β’ b = x β’ y β’ bmul_smul cβ: ?m.61545cβ cβ: ?m.61548cβ (x: ?m.61551x : M: Type vM)
#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 uR p: SubMulAction R Mp :=
p: SubMulAction R Mp.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 βmval_image_orbit {p: SubMulAction R Mp : SubMulAction: (R : Type ?u.65229) β (M : Type ?u.65228) β [inst : SMul R M] β Type ?u.65228SubMulAction R: Type uR M: Type vM} (m: { x // x β p }m : p: SubMulAction R Mp) :
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 uR m: { x // x β p }m = MulAction.orbit: (Ξ± : Type ?u.66083) β {Ξ² : Type ?u.66082} β [inst : Monoid Ξ±] β [inst : MulAction Ξ± Ξ²] β Ξ² β Set Ξ²MulAction.orbit R: Type uR (m: { x // x β p }m : M: Type vM) :=
(Set.range_comp: β {Ξ± : Type ?u.66201} {Ξ² : Type ?u.66199} {ΞΉ : Sort ?u.66200} (g : Ξ± β Ξ²) (f : ΞΉ β Ξ±),
Set.range (g β f) = g '' Set.range fSet.range_comp _: ?m.66202 β ?m.66203_ _: ?m.66204 β ?m.66202_).symm: β {Ξ± : Sort ?u.66207} {a b : Ξ±}, a = b β b = asymm
#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 βmSubMulAction.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 βmstabilizer_of_subMul.submonoid {p: SubMulAction R Mp : SubMulAction: (R : Type ?u.66278) β (M : Type ?u.66277) β [inst : SMul R M] β Type ?u.66277SubMulAction R: Type uR M: Type vM} (m: { x // x β p }m : p: SubMulAction R Mp) :
MulAction.Stabilizer.submonoid: (Ξ± : Type ?u.67021) β {Ξ² : Type ?u.67020} β [inst : Monoid Ξ±] β [inst_1 : MulAction Ξ± Ξ²] β Ξ² β Submonoid Ξ±MulAction.Stabilizer.submonoid R: Type uR 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 uR (m: { x // x β p }m : M: Type vM) := byGoals accomplished! π
S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Monoid Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R βmextS: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Monoid Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }xβ: Rhxβ β MulAction.Stabilizer.submonoid R m β xβ β MulAction.Stabilizer.submonoid R βm
S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Monoid Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R βmsimp only [MulAction.mem_stabilizer_submonoid_iff: β (Ξ± : Type ?u.67535) {Ξ² : Type ?u.67534} [inst : Monoid Ξ±] [inst_1 : MulAction Ξ± Ξ²] {b : Ξ²} {a : Ξ±},
a β MulAction.Stabilizer.submonoid Ξ± b β a β’ b = bMulAction.mem_stabilizer_submonoid_iff, β SubMulAction.val_smul: β {R : Type ?u.67570} {M : Type ?u.67569} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : { x // x β p }),
β(r β’ x) = r β’ βxSubMulAction.val_smul, SetLike.coe_eq_coe: β {A : Type ?u.67597} {B : Type ?u.67596} [i : SetLike A B] {p : A} {x y : { x // x β p }}, βx = βy β x = ySetLike.coe_eq_coe]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 βmSubMulAction.stabilizer_of_subMul.submonoid

end MulActionMonoid

section MulActionGroup

variable [Group: Type ?u.68990 β Type ?u.68990Group R: Type uR] [MulAction: (Ξ± : Type ?u.68994) β Type ?u.68993 β [inst : Monoid Ξ±] β Type (max?u.68994?u.68993)MulAction R: Type uR M: Type vM]

/-- 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 βmstabilizer_of_subMul {p: SubMulAction R Mp : SubMulAction: (R : Type ?u.69284) β (M : Type ?u.69283) β [inst : SMul R M] β Type ?u.69283SubMulAction R: Type uR M: Type vM} (m: { x // x β p }m : p: SubMulAction R Mp) :
MulAction.stabilizer: (Ξ± : Type ?u.70303) β {Ξ² : Type ?u.70302} β [inst : Group Ξ±] β [inst_1 : MulAction Ξ± Ξ²] β Ξ² β Subgroup Ξ±MulAction.stabilizer R: Type uR m: { x // x β p }m = MulAction.stabilizer: (Ξ± : Type ?u.70581) β {Ξ² : Type ?u.70580} β [inst : Group Ξ±] β [inst_1 : MulAction Ξ± Ξ²] β Ξ² β Subgroup Ξ±MulAction.stabilizer R: Type uR (m: { x // x β p }m : M: Type vM) := byGoals accomplished! π
S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Group Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }MulAction.stabilizer R m = MulAction.stabilizer R βmrw [S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Group Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }MulAction.stabilizer R m = MulAction.stabilizer R βmβ Subgroup.toSubmonoid_eq: β {G : Type ?u.70702} [inst : Group G] {p q : Subgroup G}, p.toSubmonoid = q.toSubmonoid β p = qSubgroup.toSubmonoid_eqS: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Group Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }(MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R βm).toSubmonoid]S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Group Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }(MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R βm).toSubmonoid
S: Type u'T: Type u''R: Type uM: Type vinstβΒΉ: Group Rinstβ: MulAction R Mp: SubMulAction R Mm: { x // x β p }MulAction.stabilizer R m = MulAction.stabilizer R βmexact stabilizer_of_subMul.submonoid: β {R : Type ?u.70777} {M : Type ?u.70776} [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 βmstabilizer_of_subMul.submonoid m: { x // x β p }mGoals 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 βmSubMulAction.stabilizer_of_subMul

end MulActionGroup

section Module

variable [Semiring: Type ?u.70828 β Type ?u.70828Semiring R: Type uR] [AddCommMonoid: Type ?u.70831 β Type ?u.70831AddCommMonoid M: Type vM]

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 uR M: Type vM]

variable (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.71787) β (M : Type ?u.71786) β [inst : SMul R M] β Type ?u.71786SubMulAction R: Type uR M: Type vM)

theorem zero_mem: Set.Nonempty βp β 0 β pzero_mem (h: Set.Nonempty βph : (p: SubMulAction R Mp : Set: Type ?u.72619 β Type ?u.72619Set M: Type vM).Nonempty: {Ξ± : Type ?u.72726} β Set Ξ± β PropNonempty) : (0: ?m.727530 : M: Type vM) β p: SubMulAction R Mp :=
let β¨x: Mx, hx: x β βphxβ© := h: Set.Nonempty βph
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 = 0zero_smul R: Type uR (x: Mx : M: Type vM) βΈ p: SubMulAction R Mp.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 β psmul_mem 0: ?m.740770 hx: x β βphx
#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 β pSubMulAction.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_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 β PropNonempty p: SubMulAction R Mp] : Zero: Type ?u.75981 β Type ?u.75981Zero p: SubMulAction R Mp where
zero := β¨0: ?m.761360, n_empty: Nonempty { x // x β p }n_empty.elim: β {Ξ± : Sort ?u.76713} {p : Prop}, Nonempty Ξ± β (Ξ± β p) β pelim fun x: ?m.76722x => p: SubMulAction R Mp.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 β pzero_mem β¨x: ?m.76722x, x: ?m.76722x.prop: β {Ξ± : Sort ?u.76921} {p : Ξ± β Prop} (x : Subtype p), p βxpropβ©β©

end Module

variable [Ring: Type ?u.77079 β Type ?u.77079Ring R: Type uR] [AddCommGroup: Type ?u.77082 β Type ?u.77082AddCommGroup M: Type vM]

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 uR M: Type vM]

variable (p: SubMulAction R Mp p': SubMulAction R Mp' : SubMulAction: (R : Type ?u.79277) β (M : Type ?u.79276) β [inst : SMul R M] β Type ?u.79276SubMulAction R: Type uR M: Type vM)

variable {r: Rr : R: Type uR} {x: Mx y: My : M: Type vM}

theorem neg_mem: x β p β -x β pneg_mem (hx: x β phx : x: Mx β p: SubMulAction R Mp) : -x: Mx β p: SubMulAction R Mp := byGoals accomplished! π
S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mhx: x β p-x β prw [S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mhx: x β p-x β pβ neg_one_smul: β (R : Type ?u.82775) {M : Type ?u.82774} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M),
-1 β’ x = -xneg_one_smul R: Type uRS: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mhx: x β p-1 β’ x β p]S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mhx: x β p-1 β’ x β p
S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mhx: x β p-x β pexact p: SubMulAction R Mp.smul_mem: β {R : Type ?u.82877} {M : Type ?u.82876} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R), x β p β r β’ x β psmul_mem _: ?m.82885_ hx: x β phxGoals 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 β pSubMulAction.neg_mem

@[simp]
theorem neg_mem_iff: -x β p β x β pneg_mem_iff : -x: Mx β p: SubMulAction R Mp β x: Mx β p: SubMulAction R Mp :=
β¨fun h: ?m.85870h => byGoals accomplished! π
S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mh: -x β px β prw [S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mh: -x β px β pβ neg_neg: β {G : Type ?u.86015} [inst : InvolutiveNeg G] (a : G), - -a = aneg_neg x: MxS: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mh: -x β p- -x β p]S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mh: -x β p- -x β p
S: Type u'T: Type u''R: Type uM: Type vinstβΒ²: Ring RinstβΒΉ: AddCommGroup Minstβ: Module R Mp, p': SubMulAction R Mr: Rx, y: Mh: -x β px β pexact neg_mem: β {R : Type ?u.86620} {M : Type ?u.86619} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(p : SubMulAction R M) {x : M}, x β p β -x β pneg_mem _: SubMulAction ?m.86621 ?m.86622_ h: -x β phGoals 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 β pneg_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 β pSubMulAction.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.88383Neg p: SubMulAction R Mp :=
β¨fun x: ?m.88552x => β¨-x: ?m.88552x.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 β pneg_mem _: SubMulAction ?m.88711 ?m.88712_ x: ?m.88552x.2: β {Ξ± : Sort ?u.88837} {p : Ξ± β Prop} (self : Subtype p), p βself2β©β©

@[simp, norm_cast]
theorem val_neg: β (x : { x // x β p }), β(-x) = -βxval_neg (x: { x // x β p }x : p: SubMulAction R Mp) : ((-x: { x // x β p }x : p: SubMulAction R Mp) : M: Type vM) = -x: { x // x β p }x :=
rfl: β {Ξ± : Sort ?u.91230} {a : Ξ±}, a = arfl
#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) = -βxSubMulAction.val_neg

end SubMulAction

namespace SubMulAction

variable [GroupWithZero: Type ?u.95321 β Type ?u.95321GroupWithZero S: Type u'S] [Monoid: Type ?u.93077 β Type ?u.93077Monoid R: Type uR] [MulAction: (Ξ± : Type ?u.91395) β Type ?u.91394 β [inst : Monoid Ξ±] β Type (max?u.91395?u.91394)MulAction R: Type uR M: Type vM]

variable [SMul: Type ?u.93094 β Type ?u.93093 β Type (max?u.93094?u.93093)SMul S: Type u'S R: Type uR] [MulAction: (Ξ± : Type ?u.95345) β Type ?u.95344 β [inst : Monoid Ξ±] β Type (max?u.95345?u.95344)MulAction S: Type u'S M: Type vM] [IsScalarTower: (M : Type ?u.91629) β
(N : Type ?u.91628) β (Ξ± : Type ?u.91627) β [inst : SMul M N] β [inst : SMul N Ξ±] β [inst : SMul M Ξ±] β PropIsScalarTower S: Type u'S R: Type uR M: Type vM]

variable (p: SubMulAction R Mp : SubMulAction: (R : Type ?u.97000) β (M : Type ?u.96999) β [inst : SMul R M] β Type ?u.96999SubMulAction R: Type uR M: Type vM) {s: Ss : S: Type u'S} {x: Mx y: My : M: Type vM}

theorem smul_mem_iff: s β  0 β (s β’ x β p β x β p)smul_mem_iff (s0: s β  0s0 : s: Ss β  0: ?m.975630) : s: Ss β’ x: Mx β p: SubMulAction R Mp β x: Mx β p: SubMulAction R Mp :=
p: SubMulAction R Mp.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 β psmul_mem_iff' (Units.mk0: {Gβ : Type ?u.98805} β [inst : GroupWithZero Gβ] β (a : Gβ) β a β  0 β GβΛ£Units.mk0 s: Ss s0: s β  0s0)
#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
```