Ordered instances on submonoids

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : { x : M // x ∈ s }) => ↑a

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_1 {M : Type u_2} {S : Type u_1} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

@[instance 75]

instance AddSubmonoidClass.toOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedAddCommMonoid { x : M // x ∈ s }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedAddCommMonoid s = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : { x : M // x ∈ s }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

@[instance 75]

instance SubmonoidClass.toOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCommMonoid { x : M // x ∈ s }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• SubmonoidClass.toOrderedCommMonoid s = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : { x : M // x ∈ s }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_2} {S : Type u_1} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedAddCommMonoid { x : M // x ∈ s }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedAddCommMonoid s = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : { x : M // x ∈ s }) => ↑a

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

@[instance 75]

instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCommMonoid { x : M // x ∈ s }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCommMonoid s = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : { x : M // x ∈ s }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_2} {S : Type u_1} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : { x : M // x ∈ s }) => ↑a

@[instance 75]

instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedCancelAddCommMonoid { x : M // x ∈ s }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedCancelAddCommMonoid s = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x + x_1) = ↑(x + x_1)

@[instance 75]

instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCancelCommMonoid { x : M // x ∈ s }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• SubmonoidClass.toOrderedCancelCommMonoid s = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_2} {S : Type u_1} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] : ZeroMemClass S M

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) : ∀ (x x_1 : { x : M // x ∈ s }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ∀ (x : { x : M // x ∈ s }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) : Function.Injective fun (a : { x : M // x ∈ s }) => ↑a

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : ↑0 = ↑0

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedCancelAddCommMonoid { x : M // x ∈ s }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid s = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCancelCommMonoid { x : M // x ∈ s }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCancelCommMonoid s = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_2 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : { x : M // x ∈ S }) => ↑a

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_1 {M : Type u_1} [OrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_3 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x : M // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoid.toOrderedAddCommMonoid {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : OrderedAddCommMonoid { x : M // x ∈ S }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• S.toOrderedAddCommMonoid = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toOrderedCommMonoid {M : Type u_1} [OrderedCommMonoid M] (S : Submonoid M) : OrderedCommMonoid { x : M // x ∈ S }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• S.toOrderedCommMonoid = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x : M // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : { x : M // x ∈ S }) => ↑a

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

instance AddSubmonoid.toLinearOrderedAddCommMonoid {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedAddCommMonoid { x : M // x ∈ S }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• S.toLinearOrderedAddCommMonoid = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

instance Submonoid.toLinearOrderedCommMonoid {M : Type u_1} [LinearOrderedCommMonoid M] (S : Submonoid M) : LinearOrderedCommMonoid { x : M // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• S.toLinearOrderedCommMonoid = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [OrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x : M // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : { x : M // x ∈ S }) => ↑a

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoid.toOrderedCancelAddCommMonoid {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : OrderedCancelAddCommMonoid { x : M // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• S.toOrderedCancelAddCommMonoid = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toOrderedCancelCommMonoid {M : Type u_1} [OrderedCancelCommMonoid M] (S : Submonoid M) : OrderedCancelCommMonoid { x : M // x ∈ S }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• S.toOrderedCancelCommMonoid = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance AddSubmonoid.toLinearOrderedCancelAddCommMonoid {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedCancelAddCommMonoid { x : M // x ∈ S }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• S.toLinearOrderedCancelAddCommMonoid = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x : M // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : { x : M // x ∈ S }) => ↑a

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : M // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance Submonoid.toLinearOrderedCancelCommMonoid {M : Type u_1} [LinearOrderedCancelCommMonoid M] (S : Submonoid M) : LinearOrderedCancelCommMonoid { x : M // x ∈ S }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• S.toLinearOrderedCancelCommMonoid = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.nonneg.proof_2 (M : Type u_1) [AddMonoid M] [Preorder M] : 0 ≤ 0

def AddSubmonoid.nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] : AddSubmonoid M

The submonoid of nonnegative elements.

Equations

• AddSubmonoid.nonneg M = { carrier := Set.Ici 0, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddSubmonoid.nonneg.proof_1 (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] : ∀ {a b : M}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b

@[simp]

theorem Submonoid.oneLE_coe (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] : ↑(Submonoid.oneLE M) = Set.Ici 1

@[simp]

theorem AddSubmonoid.nonneg_coe (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] : ↑(AddSubmonoid.nonneg M) = Set.Ici 0

def Submonoid.oneLE (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] : Submonoid M

The submonoid of elements greater than 1.

Equations

• Submonoid.oneLE M = { carrier := Set.Ici 1, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.mem_nonneg {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {a : M} : a ∈ AddSubmonoid.nonneg M ↔ 0 ≤ a

@[simp]

theorem Submonoid.mem_oneLE {M : Type u_1} [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {a : M} : a ∈ Submonoid.oneLE M ↔ 1 ≤ a