# Subsemigroups: definition #

This file defines bundled multiplicative and additive subsemigroups.

## Main definitions #

- `Subsemigroup M`: the type of bundled subsemigroup of a magma `M`; the underlying set is given in the `carrier` field of the structure, and should be accessed through coercion as in `(S : Set M)`.
- `AddSubsemigroup M` : the type of bundled subsemigroups of an additive magma `M`.

For each of the following definitions in the `Subsemigroup` namespace, there is a corresponding definition in the `AddSubsemigroup` namespace.

- `Subsemigroup.copy` : copy of a subsemigroup with `carrier` replaced by a set that is equal but possibly not definitionally equal to the carrier of the original `Subsemigroup`.

Similarly, for each of these definitions in the `MulHom` namespace, there is a corresponding definition in the `AddHom` namespace.

- `MulHom.eqLocus f g`: the subsemigroup of those `x` such that `f x = g x`

## Implementation notes #

Subsemigroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as membership of a subsemigroup's underlying set.

Note that `Subsemigroup M` does not actually require `Semigroup M`, instead requiring only the weaker `Mul M`.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

## Tags #

subsemigroup, subsemigroups

source
class MulMemClass (S : Type u_3) (M : outParam (Type u_4)) [Mul M] [SetLike S M] :
Prop

`MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)`

- mul_mem {s : S} {a b : M} : a ∈ s → b ∈ s → a * b ∈ s

  A substructure satisfying `MulMemClass` is closed under multiplication.

Instances

source
class AddMemClass (S : Type u_3) (M : outParam (Type u_4)) [Add M] [SetLike S M] :
Prop

`AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)`

- add_mem {s : S} {a b : M} : a ∈ s → b ∈ s → a + b ∈ s

  A substructure satisfying `AddMemClass` is closed under addition.

Instances

source
structure Subsemigroup (M : Type u_3) [Mul M] :
Type u_3

A subsemigroup of a magma `M` is a subset closed under multiplication.

- carrier : Set M

  The carrier of a subsemigroup.

- mul_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier

  The product of two elements of a subsemigroup belongs to the subsemigroup.

Instances For

source
structure AddSubsemigroup (M : Type u_3) [Add M] :
Type u_3

An additive subsemigroup of an additive magma `M` is a subset closed under addition.

- carrier : Set M

  The carrier of an additive subsemigroup.

- add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier

  The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

Instances For

source
instance Subsemigroup.instSetLike {M : Type u_1} [Mul M] :
SetLike (Subsemigroup M) M
Equations

- Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := ⋯ }

source
instance AddSubsemigroup.instSetLike {M : Type u_1} [Add M] :
SetLike (AddSubsemigroup M) M
Equations

- AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective' := ⋯ }

source
def Subsemigroup.ofClass {S : Type u_3} {M : Type u_4} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) :
Subsemigroup M

The actual `Subsemigroup` obtained from an element of a `MulMemClass`.

Equations

- Subsemigroup.ofClass s = { carrier := ↑s, mul_mem' := ⋯ }

Instances For

source
def AddSubsemigroup.ofClass {S : Type u_3} {M : Type u_4} [Add M] [SetLike S M] [AddMemClass S M] (s : S) :
AddSubsemigroup M

The actual `AddSubsemigroup` obtained from an element of a `AddMemClass`

Equations

- AddSubsemigroup.ofClass s = { carrier := ↑s, add_mem' := ⋯ }

Instances For

source
@[simp]
theorem AddSubsemigroup.coe_ofClass {S : Type u_3} {M : Type u_4} [Add M] [SetLike S M] [AddMemClass S M] (s : S) :
↑(ofClass s) = ↑s
source
@[simp]
theorem Subsemigroup.coe_ofClass {S : Type u_3} {M : Type u_4} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) :
↑(ofClass s) = ↑s
source
@[instance 100]
instance Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul {M : Type u_1} [Mul M] :
CanLift (Set M) (Subsemigroup M) SetLike.coe fun (s : Set M) => ∀ {x y : M}, x ∈ s → y ∈ s → x * y ∈ s
source
@[instance 100]
instance AddSubsemigroup.instCanLiftSetCoeForallForallForallMemForallHAdd {M : Type u_1} [Add M] :
CanLift (Set M) (AddSubsemigroup M) SetLike.coe fun (s : Set M) => ∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s
source
instance Subsemigroup.instMulMemClass {M : Type u_1} [Mul M] :
MulMemClass (Subsemigroup M) M
source
instance AddSubsemigroup.instAddMemClass {M : Type u_1} [Add M] :
AddMemClass (AddSubsemigroup M) M
source
@[simp]
theorem Subsemigroup.mem_carrier {M : Type u_1} [Mul M] {s : Subsemigroup M} {x : M} :
x ∈ s.carrier ↔ x ∈ s
source
@[simp]
theorem AddSubsemigroup.mem_carrier {M : Type u_1} [Add M] {s : AddSubsemigroup M} {x : M} :
x ∈ s.carrier ↔ x ∈ s
source
@[simp]
theorem Subsemigroup.mem_mk {M : Type u_1} [Mul M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :
x ∈ { carrier := s, mul_mem' := h_mul } ↔ x ∈ s
source
@[simp]
theorem AddSubsemigroup.mem_mk {M : Type u_1} [Add M] {s : Set M} {x : M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :
x ∈ { carrier := s, add_mem' := h_add } ↔ x ∈ s
source
@[simp]
theorem Subsemigroup.coe_set_mk {M : Type u_1} [Mul M] (s : Set M) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :
↑{ carrier := s, mul_mem' := h_mul } = s
source
@[simp]
theorem AddSubsemigroup.coe_set_mk {M : Type u_1} [Add M] (s : Set M) (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :
↑{ carrier := s, add_mem' := h_add } = s
source
@[simp]
theorem Subsemigroup.mk_le_mk {M : Type u_1} [Mul M] {s t : Set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t) :
{ carrier := s, mul_mem' := h_mul } ≤ { carrier := t, mul_mem' := h_mul' } ↔ s ⊆ t
source
@[simp]
theorem AddSubsemigroup.mk_le_mk {M : Type u_1} [Add M] {s t : Set M} (h_add : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) (h_add' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t) :
{ carrier := s, add_mem' := h_add } ≤ { carrier := t, add_mem' := h_add' } ↔ s ⊆ t
source
theorem Subsemigroup.ext {M : Type u_1} [Mul M] {S T : Subsemigroup M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :
S = T

Two subsemigroups are equal if they have the same elements.

source
theorem AddSubsemigroup.ext {M : Type u_1} [Add M] {S T : AddSubsemigroup M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :
S = T

Two `AddSubsemigroup`s are equal if they have the same elements.

source
theorem Subsemigroup.ext_iff {M : Type u_1} [Mul M] {S T : Subsemigroup M} :
S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
source
theorem AddSubsemigroup.ext_iff {M : Type u_1} [Add M] {S T : AddSubsemigroup M} :
S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
source
def Subsemigroup.copy {M : Type u_1} [Mul M] (S : Subsemigroup M) (s : Set M) (hs : s = ↑S) :
Subsemigroup M

Copy a subsemigroup replacing `carrier` with a set that is equal to it.

Equations

- S.copy s hs = { carrier := s, mul_mem' := ⋯ }

Instances For

source
def AddSubsemigroup.copy {M : Type u_1} [Add M] (S : AddSubsemigroup M) (s : Set M) (hs : s = ↑S) :
AddSubsemigroup M

Copy an additive subsemigroup replacing `carrier` with a set that is equal to it.

Equations

- S.copy s hs = { carrier := s, add_mem' := ⋯ }

Instances For

source
@[simp]
theorem Subsemigroup.coe_copy {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) :
↑(S.copy s hs) = s
source
@[simp]
theorem AddSubsemigroup.coe_copy {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S) :
↑(S.copy s hs) = s
source
theorem Subsemigroup.copy_eq {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) :
S.copy s hs = S
source
theorem AddSubsemigroup.copy_eq {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = ↑S) :
S.copy s hs = S
source
theorem Subsemigroup.mul_mem {M : Type u_1} [Mul M] (S : Subsemigroup M) {x y : M} :
x ∈ S → y ∈ S → x * y ∈ S

A subsemigroup is closed under multiplication.

source
theorem AddSubsemigroup.add_mem {M : Type u_1} [Add M] (S : AddSubsemigroup M) {x y : M} :
x ∈ S → y ∈ S → x + y ∈ S

An `AddSubsemigroup` is closed under addition.

source
instance Subsemigroup.instTop {M : Type u_1} [Mul M] :
Top (Subsemigroup M)

The subsemigroup `M` of the magma `M`.

Equations

- Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯ } }

source
instance AddSubsemigroup.instTop {M : Type u_1} [Add M] :
Top (AddSubsemigroup M)

The additive subsemigroup `M` of the magma `M`.

Equations

- AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := ⋯ } }

source
instance Subsemigroup.instBot {M : Type u_1} [Mul M] :
Bot (Subsemigroup M)

The trivial subsemigroup `∅` of a magma `M`.

Equations

- Subsemigroup.instBot = { bot := { carrier := ∅, mul_mem' := ⋯ } }

source
instance AddSubsemigroup.instBot {M : Type u_1} [Add M] :
Bot (AddSubsemigroup M)

The trivial `AddSubsemigroup` `∅` of an additive magma `M`.

Equations

- AddSubsemigroup.instBot = { bot := { carrier := ∅, add_mem' := ⋯ } }

source
instance Subsemigroup.instInhabited {M : Type u_1} [Mul M] :
Inhabited (Subsemigroup M)
Equations

- Subsemigroup.instInhabited = { default := ⊥ }

source
instance AddSubsemigroup.instInhabited {M : Type u_1} [Add M] :
Inhabited (AddSubsemigroup M)
Equations

- AddSubsemigroup.instInhabited = { default := ⊥ }

source
theorem Subsemigroup.notMem_bot {M : Type u_1} [Mul M] {x : M} :
x ∉ ⊥
source
theorem AddSubsemigroup.notMem_bot {M : Type u_1} [Add M] {x : M} :
x ∉ ⊥
source
@[deprecated AddSubsemigroup.notMem_bot (since := "2025-05-23")]
theorem AddSubsemigroup.not_mem_bot {M : Type u_1} [Add M] {x : M} :
x ∉ ⊥

Alias of `AddSubsemigroup.notMem_bot`.

source
@[deprecated Subsemigroup.notMem_bot (since := "2025-05-23")]
theorem Subsemigroup.not_mem_bot {M : Type u_1} [Mul M] {x : M} :
x ∉ ⊥

Alias of `Subsemigroup.notMem_bot`.

source
@[simp]
theorem Subsemigroup.mem_top {M : Type u_1} [Mul M] (x : M) :
x ∈ ⊤
source
@[simp]
theorem AddSubsemigroup.mem_top {M : Type u_1} [Add M] (x : M) :
x ∈ ⊤
source
@[simp]
theorem Subsemigroup.coe_top {M : Type u_1} [Mul M] :
↑⊤ = Set.univ
source
@[simp]
theorem AddSubsemigroup.coe_top {M : Type u_1} [Add M] :
↑⊤ = Set.univ
source
@[simp]
theorem Subsemigroup.coe_bot {M : Type u_1} [Mul M] :
↑⊥ = ∅
source
@[simp]
theorem AddSubsemigroup.coe_bot {M : Type u_1} [Add M] :
↑⊥ = ∅
source
instance Subsemigroup.instMin {M : Type u_1} [Mul M] :
Min (Subsemigroup M)

The inf of two subsemigroups is their intersection.

Equations

- Subsemigroup.instMin = { min := fun (S₁ S₂ : Subsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯ } }

source
instance AddSubsemigroup.instMin {M : Type u_1} [Add M] :
Min (AddSubsemigroup M)

The inf of two `AddSubsemigroup`s is their intersection.

Equations

- AddSubsemigroup.instMin = { min := fun (S₁ S₂ : AddSubsemigroup M) => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯ } }

source
@[simp]
theorem Subsemigroup.coe_inf {M : Type u_1} [Mul M] (p p' : Subsemigroup M) :
↑(p ⊓ p') = ↑p ∩ ↑p'
source
@[simp]
theorem AddSubsemigroup.coe_inf {M : Type u_1} [Add M] (p p' : AddSubsemigroup M) :
↑(p ⊓ p') = ↑p ∩ ↑p'
source
@[simp]
theorem Subsemigroup.mem_inf {M : Type u_1} [Mul M] {p p' : Subsemigroup M} {x : M} :
x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
source
@[simp]
theorem AddSubsemigroup.mem_inf {M : Type u_1} [Add M] {p p' : AddSubsemigroup M} {x : M} :
x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
source
theorem Subsemigroup.subsingleton_of_subsingleton {M : Type u_1} [Mul M] [Subsingleton (Subsemigroup M)] :
Subsingleton M
source
theorem AddSubsemigroup.subsingleton_of_subsingleton {M : Type u_1} [Add M] [Subsingleton (AddSubsemigroup M)] :
Subsingleton M
source
instance Subsemigroup.instNontrivialOfNonempty {M : Type u_1} [Mul M] [hn : Nonempty M] :
Nontrivial (Subsemigroup M)
source
instance AddSubsemigroup.instNontrivialOfNonempty {M : Type u_1} [Add M] [hn : Nonempty M] :
Nontrivial (AddSubsemigroup M)
source
def MulHom.eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f g : M →ₙ* N) :
Subsemigroup M

The subsemigroup of elements `x : M` such that `f x = g x`

Equations

- f.eqLocus g = { carrier := {x : M | f x = g x}, mul_mem' := ⋯ }

Instances For

source
def AddHom.eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f g : M →ₙ+ N) :
AddSubsemigroup M

The additive subsemigroup of elements `x : M` such that `f x = g x`

Equations

- f.eqLocus g = { carrier := {x : M | f x = g x}, add_mem' := ⋯ }

Instances For

source
@[simp]
theorem MulHom.mem_eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f g : M →ₙ* N} {x : M} :
x ∈ f.eqLocus g ↔ f x = g x
source
@[simp]
theorem AddHom.mem_eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f g : M →ₙ+ N} {x : M} :
x ∈ f.eqLocus g ↔ f x = g x
source
theorem MulHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f g : M →ₙ* N} (h : Set.EqOn ⇑f ⇑g ↑⊤) :
f = g
source
theorem AddHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f g : M →ₙ+ N} (h : Set.EqOn ⇑f ⇑g ↑⊤) :
f = g
source
@[instance 900]
instance MulMemClass.mul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
Mul ↥S'

A submagma of a magma inherits a multiplication.

Equations

- MulMemClass.mul S' = { mul := fun (a b : ↥S') => ⟨↑a * ↑b, ⋯⟩ }

source
@[instance 900]
instance AddMemClass.add {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
Add ↥S'

An additive submagma of an additive magma inherits an addition.

Equations

- AddMemClass.add S' = { add := fun (a b : ↥S') => ⟨↑a + ↑b, ⋯⟩ }

source
@[simp]
theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S') :
↑(x * y) = ↑x * ↑y
source
@[simp]
theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S') :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') :
⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
source
@[simp]
theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') :
⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
source
theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S') :
x * y = ⟨↑x * ↑y, ⋯⟩
source
theorem AddMemClass.add_def {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S') :
x + y = ⟨↑x + ↑y, ⋯⟩
source
instance MulMemClass.toSemigroup {M : Type u_4} [Semigroup M] {A : Type u_5} [SetLike A M] [MulMemClass A M] (S : A) :
Semigroup ↥S

A subsemigroup of a semigroup inherits a semigroup structure.

Equations

- MulMemClass.toSemigroup S = { toMul := MulMemClass.mul S, mul_assoc := ⋯ }

source
instance AddMemClass.toAddSemigroup {M : Type u_4} [AddSemigroup M] {A : Type u_5} [SetLike A M] [AddMemClass A M] (S : A) :
AddSemigroup ↥S

An `AddSubsemigroup` of an `AddSemigroup` inherits an `AddSemigroup` structure.

Equations

- AddMemClass.toAddSemigroup S = { toAdd := AddMemClass.add S, add_assoc := ⋯ }

source
instance MulMemClass.toCommSemigroup {M : Type u_5} [CommSemigroup M] {A : Type u_4} [SetLike A M] [MulMemClass A M] (S : A) :
CommSemigroup ↥S

A subsemigroup of a `CommSemigroup` is a `CommSemigroup`.

Equations

- MulMemClass.toCommSemigroup S = { toSemigroup := MulMemClass.toSemigroup S, mul_comm := ⋯ }

source
instance AddMemClass.toAddCommSemigroup {M : Type u_5} [AddCommSemigroup M] {A : Type u_4} [SetLike A M] [AddMemClass A M] (S : A) :
AddCommSemigroup ↥S

An `AddSubsemigroup` of an `AddCommSemigroup` is an `AddCommSemigroup`.

Equations

- AddMemClass.toAddCommSemigroup S = { toAddSemigroup := AddMemClass.toAddSemigroup S, add_comm := ⋯ }

source
instance MulMemClass.isLeftCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsLeftCancelMul M] (S : A) :
IsLeftCancelMul ↥S

A submagma of a left cancellative magma inherits left cancellation.

source
instance AddMemClass.isLeftCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsLeftCancelAdd M] (S : A) :
IsLeftCancelAdd ↥S

An additive submagma of a left cancellative additive magma inherits left cancellation.

source
instance MulMemClass.isRightCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsRightCancelMul M] (S : A) :
IsRightCancelMul ↥S

A submagma of a right cancellative magma inherits right cancellation.

source
instance AddMemClass.isRightCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsRightCancelAdd M] (S : A) :
IsRightCancelAdd ↥S

An additive submagma of a right cancellative additive magma inherits right cancellation.

source
instance MulMemClass.isCancelMul {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] [IsCancelMul M] (S : A) :
IsCancelMul ↥S

A submagma of a cancellative magma inherits cancellation.

source
instance AddMemClass.isCancelAdd {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] [IsCancelAdd M] (S : A) :
IsCancelAdd ↥S

An additive submagma of a cancellative additive magma inherits cancellation.

source
def MulMemClass.subtype {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
↥S' →ₙ* M

The natural semigroup hom from a subsemigroup of semigroup `M` to `M`.

Equations

- MulMemClass.subtype S' = { toFun := Subtype.val, map_mul' := ⋯ }

Instances For

source
def AddMemClass.subtype {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
↥S' →ₙ+ M

The natural semigroup hom from an `AddSubsemigroup` of `AddSubsemigroup` `M` to `M`.

Equations

- AddMemClass.subtype S' = { toFun := Subtype.val, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MulMemClass.subtype_apply {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] {S' : A} (x : ↥S') :
(subtype S') x = ↑x
source
@[simp]
theorem AddMemClass.subtype_apply {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] {S' : A} (x : ↥S') :
(subtype S') x = ↑x
source
theorem MulMemClass.subtype_injective {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
Function.Injective ⇑(subtype S')
source
theorem AddMemClass.subtype_injective {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
Function.Injective ⇑(subtype S')
source
@[simp]
theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_3} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
⇑(subtype S') = Subtype.val
source
@[simp]
theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
⇑(subtype S') = Subtype.val