Subsemigroups: definition and complete_lattice structure

This file defines bundled multiplicative and additive subsemigroups. We also define a CompleteLattice structure on Subsemigroups, and define the closure of a set as the minimal subsemigroup that includes this set.

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.
• Subsemigroup.closure : semigroup closure of a set, i.e., the least subsemigroup that includes the set.
• Subsemigroup.gi : closure : Set M → Subsemigroup M→ Subsemigroup M and coercion coe : Subsemigroup M → Set M→ Set M form a GaloisInsertion;

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

ink

class MulMemClass (S : Type u_1) (M : Type u_2) [inst : Mul M] [inst : SetLike S M] : Prop

• A substructure satisfying MulMemClass is closed under multiplication.

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

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

ink

class AddMemClass (S : Type u_1) (M : Type u_2) [inst : Add M] [inst : SetLike S M] : Prop

• A substructure satisfying AddMemClass is closed under addition.

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

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

ink

structure Subsemigroup (M : Type u_1) [inst : Mul M] : Type u_1

• The carrier of a subsemigroup.

  carrier : Set M

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

  mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier

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

ink

structure AddSubsemigroup (M : Type u_1) [inst : Add M] : Type u_1

• The carrier of an additive subsemigroup.

  carrier : Set M

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

  add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier

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

ink

def AddSubsemigroup.instSetLikeSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] (p : AddSubsemigroup M) (q : AddSubsemigroup M) (h : p.carrier = q.carrier) : p = q

Equations

• (_ : p = q) = (_ : p = q)

ink

instance AddSubsemigroup.instSetLikeSubsemigroup {M : Type u_1} [inst : Add M] : SetLike (AddSubsemigroup M) M

Equations

• AddSubsemigroup.instSetLikeSubsemigroup = { coe := AddSubsemigroup.carrier, coe_injective' := (_ : ∀ (p q : AddSubsemigroup M), p.carrier = q.carrier → p = q) }

ink

instance Subsemigroup.instSetLikeSubsemigroup {M : Type u_1} [inst : Mul M] : SetLike (Subsemigroup M) M

Equations

• Subsemigroup.instSetLikeSubsemigroup = { coe := Subsemigroup.carrier, coe_injective' := (_ : ∀ (p q : Subsemigroup M), p.carrier = q.carrier → p = q) }

ink

instance AddSubsemigroup.instAddMemClassSubsemigroupInstSetLikeSubsemigroup {M : Type u_1} [inst : Add M] : AddMemClass (AddSubsemigroup M) M

Equations

• @AddSubsemigroup.instAddMemClassSubsemigroupInstSetLikeSubsemigroup = @AddSubsemigroup.instAddMemClassSubsemigroupInstSetLikeSubsemigroup.proof_1

ink

def AddSubsemigroup.instAddMemClassSubsemigroupInstSetLikeSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] : AddMemClass (AddSubsemigroup M) M

Equations

• (_ : AddMemClass (AddSubsemigroup M) M) = (_ : AddMemClass (AddSubsemigroup M) M)

ink

instance Subsemigroup.instMulMemClassSubsemigroupInstSetLikeSubsemigroup {M : Type u_1} [inst : Mul M] : MulMemClass (Subsemigroup M) M

Equations

• @Subsemigroup.instMulMemClassSubsemigroupInstSetLikeSubsemigroup = @Subsemigroup.instMulMemClassSubsemigroupInstSetLikeSubsemigroup.proof_1

ink

@[simp]

theorem AddSubsemigroup.mem_carrier {M : Type u_1} [inst : Add M] {s : AddSubsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s

ink

@[simp]

theorem Subsemigroup.mem_carrier {M : Type u_1} [inst : Mul M] {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s

ink

@[simp]

theorem AddSubsemigroup.mem_mk {M : Type u_1} [inst : Add M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) : x ∈ { carrier := s, add_mem' := h_mul } ↔ x ∈ s

ink

@[simp]

theorem Subsemigroup.mem_mk {M : Type u_1} [inst : 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

ink

@[simp]

theorem AddSubsemigroup.coe_set_mk {M : Type u_1} [inst : Add M] {s : Set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) : ↑{ carrier := s, add_mem' := h_mul } = s

ink

@[simp]

theorem Subsemigroup.coe_set_mk {M : Type u_1} [inst : Mul M] {s : Set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) : ↑{ carrier := s, mul_mem' := h_mul } = s

ink

@[simp]

theorem AddSubsemigroup.mk_le_mk {M : Type u_1} [inst : Add M] {s : Set M} {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, add_mem' := h_mul } ≤ { carrier := t, add_mem' := h_mul' } ↔ s ⊆ t

ink

@[simp]

theorem Subsemigroup.mk_le_mk {M : Type u_1} [inst : Mul M] {s : Set M} {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

ink

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

Two AddSubsemigroups are equal if they have the same elements.

ink

theorem Subsemigroup.ext {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) : S = T

Two subsemigroups are equal if they have the same elements.

ink

def AddSubsemigroup.copy {M : Type u_1} [inst : 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

• AddSubsemigroup.copy S s hs = { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }

ink

def AddSubsemigroup.copy.proof_1 {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) (s : Set M) (hs : s = ↑S) : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

Equations

• (_ : a ∈ s → b ∈ s → a + b ∈ s) = (_ : a ∈ s → b ∈ s → a + b ∈ s)

ink

def Subsemigroup.copy {M : Type u_1} [inst : 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

• Subsemigroup.copy S s hs = { carrier := s, mul_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) }

ink

@[simp]

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

ink

@[simp]

theorem Subsemigroup.coe_copy {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) : ↑(Subsemigroup.copy S s hs) = s

ink

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

ink

theorem Subsemigroup.copy_eq {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S) : Subsemigroup.copy S s hs = S

ink

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

An AddSubsemigroup is closed under addition.

ink

theorem Subsemigroup.mul_mem {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) {x : M} {y : M} : x ∈ S → y ∈ S → x * y ∈ S

A subsemigroup is closed under multiplication.

ink

def AddSubsemigroup.instTopSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] : ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a + b ∈ Set.univ

Equations

• (_ : a + b ∈ Set.univ) = (_ : a + b ∈ Set.univ)

ink

instance AddSubsemigroup.instTopSubsemigroup {M : Type u_1} [inst : Add M] : Top (AddSubsemigroup M)

The additive subsemigroup M of the magma M.

Equations

• AddSubsemigroup.instTopSubsemigroup = { top := { carrier := Set.univ, add_mem' := (_ : ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a + b ∈ Set.univ) } }

ink

instance Subsemigroup.instTopSubsemigroup {M : Type u_1} [inst : Mul M] : Top (Subsemigroup M)

The subsemigroup M of the magma M.

Equations

• Subsemigroup.instTopSubsemigroup = { top := { carrier := Set.univ, mul_mem' := (_ : ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a * b ∈ Set.univ) } }

ink

instance AddSubsemigroup.instBotSubsemigroup {M : Type u_1} [inst : Add M] : Bot (AddSubsemigroup M)

The trivial AddSubsemigroup ∅∅ of an additive magma M.

Equations

• AddSubsemigroup.instBotSubsemigroup = { bot := { carrier := ∅, add_mem' := (_ : ∀ {a b : M}, False → b ∈ ∅ → a + b ∈ ∅) } }

ink

def AddSubsemigroup.instBotSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] : ∀ {a b : M}, False → b ∈ ∅ → a + b ∈ ∅

Equations

• (_ : False → b ∈ ∅ → a + b ∈ ∅) = (_ : False → b ∈ ∅ → a + b ∈ ∅)

ink

instance Subsemigroup.instBotSubsemigroup {M : Type u_1} [inst : Mul M] : Bot (Subsemigroup M)

The trivial subsemigroup ∅∅ of a magma M.

Equations

• Subsemigroup.instBotSubsemigroup = { bot := { carrier := ∅, mul_mem' := (_ : ∀ {a b : M}, False → b ∈ ∅ → a * b ∈ ∅) } }

ink

instance AddSubsemigroup.instInhabitedSubsemigroup {M : Type u_1} [inst : Add M] : Inhabited (AddSubsemigroup M)

Equations

• AddSubsemigroup.instInhabitedSubsemigroup = { default := ⊥ }

ink

instance Subsemigroup.instInhabitedSubsemigroup {M : Type u_1} [inst : Mul M] : Inhabited (Subsemigroup M)

Equations

• Subsemigroup.instInhabitedSubsemigroup = { default := ⊥ }

ink

theorem AddSubsemigroup.not_mem_bot {M : Type u_1} [inst : Add M] {x : M} : ¬x ∈ ⊥

ink

theorem Subsemigroup.not_mem_bot {M : Type u_1} [inst : Mul M] {x : M} : ¬x ∈ ⊥

ink

@[simp]

theorem AddSubsemigroup.mem_top {M : Type u_1} [inst : Add M] (x : M) : x ∈ ⊤

ink

@[simp]

theorem Subsemigroup.mem_top {M : Type u_1} [inst : Mul M] (x : M) : x ∈ ⊤

ink

@[simp]

theorem AddSubsemigroup.coe_top {M : Type u_1} [inst : Add M] : ↑⊤ = Set.univ

ink

@[simp]

theorem Subsemigroup.coe_top {M : Type u_1} [inst : Mul M] : ↑⊤ = Set.univ

ink

@[simp]

theorem AddSubsemigroup.coe_bot {M : Type u_1} [inst : Add M] : ↑⊥ = ∅

ink

@[simp]

theorem Subsemigroup.coe_bot {M : Type u_1} [inst : Mul M] : ↑⊥ = ∅

ink

abbrev AddSubsemigroup.instInfSubsemigroup.match_1 {M : Type u_1} [inst : Add M] (S₁ : AddSubsemigroup M) (S₂ : AddSubsemigroup M) : {b : M} → ∀ (motive : b ∈ ↑S₁ ∩ ↑S₂ → Prop) (x : b ∈ ↑S₁ ∩ ↑S₂), (∀ (hy : b ∈ ↑S₁) (hy' : b ∈ ↑S₂), motive (_ : b ∈ ↑S₁ ∧ b ∈ ↑S₂)) → motive x

Equations

• AddSubsemigroup.instInfSubsemigroup.match_1 S₁ S₂ motive x h_1 = And.casesOn x fun left right => h_1 left right

ink

def AddSubsemigroup.instInfSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] (S₁ : AddSubsemigroup M) (S₂ : AddSubsemigroup M) : ∀ {a b : M}, a ∈ ↑S₁ ∩ ↑S₂ → b ∈ ↑S₁ ∩ ↑S₂ → a + b ∈ ↑S₁ ∩ ↑S₂

Equations

• (_ : a + b ∈ ↑S₁ ∩ ↑S₂) = (_ : a + b ∈ ↑S₁ ∩ ↑S₂)

ink

instance AddSubsemigroup.instInfSubsemigroup {M : Type u_1} [inst : Add M] : Inf (AddSubsemigroup M)

The inf of two AddSubsemigroups is their intersection.

Equations

• AddSubsemigroup.instInfSubsemigroup = { inf := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := (_ : ∀ {a b : M}, a ∈ ↑S₁ ∩ ↑S₂ → b ∈ ↑S₁ ∩ ↑S₂ → a + b ∈ ↑S₁ ∩ ↑S₂) } }

ink

instance Subsemigroup.instInfSubsemigroup {M : Type u_1} [inst : Mul M] : Inf (Subsemigroup M)

The inf of two subsemigroups is their intersection.

Equations

• Subsemigroup.instInfSubsemigroup = { inf := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑S₁ ∩ ↑S₂ → b ∈ ↑S₁ ∩ ↑S₂ → a * b ∈ ↑S₁ ∩ ↑S₂) } }

ink

@[simp]

theorem AddSubsemigroup.coe_inf {M : Type u_1} [inst : Add M] (p : AddSubsemigroup M) (p' : AddSubsemigroup M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

ink

@[simp]

theorem Subsemigroup.coe_inf {M : Type u_1} [inst : Mul M] (p : Subsemigroup M) (p' : Subsemigroup M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

ink

@[simp]

theorem AddSubsemigroup.mem_inf {M : Type u_1} [inst : Add M] {p : AddSubsemigroup M} {p' : AddSubsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

ink

@[simp]

theorem Subsemigroup.mem_inf {M : Type u_1} [inst : Mul M] {p : Subsemigroup M} {p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

ink

instance AddSubsemigroup.instInfSetSubsemigroup {M : Type u_1} [inst : Add M] : InfSet (AddSubsemigroup M)

Equations

• One or more equations did not get rendered due to their size.

ink

def AddSubsemigroup.instInfSetSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] (s : Set (AddSubsemigroup M)) : ∀ {a b : M}, (a ∈ Set.interᵢ fun t => Set.interᵢ fun h => ↑t) → (b ∈ Set.interᵢ fun t => Set.interᵢ fun h => ↑t) → a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x

Equations

• (_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)

ink

instance Subsemigroup.instInfSetSubsemigroup {M : Type u_1} [inst : Mul M] : InfSet (Subsemigroup M)

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem AddSubsemigroup.coe_infₛ {M : Type u_1} [inst : Add M] (S : Set (AddSubsemigroup M)) : ↑(infₛ S) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

ink

@[simp]

theorem Subsemigroup.coe_infₛ {M : Type u_1} [inst : Mul M] (S : Set (Subsemigroup M)) : ↑(infₛ S) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

ink

theorem AddSubsemigroup.mem_infₛ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {x : M} : x ∈ infₛ S ↔ ∀ (p : AddSubsemigroup M), p ∈ S → x ∈ p

ink

theorem Subsemigroup.mem_infₛ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)} {x : M} : x ∈ infₛ S ↔ ∀ (p : Subsemigroup M), p ∈ S → x ∈ p

ink

theorem AddSubsemigroup.mem_infᵢ {M : Type u_2} [inst : Add M] {ι : Sort u_1} {S : ι → AddSubsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ (i : ι), x ∈ S i

ink

theorem Subsemigroup.mem_infᵢ {M : Type u_2} [inst : Mul M] {ι : Sort u_1} {S : ι → Subsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ (i : ι), x ∈ S i

ink

@[simp]

theorem AddSubsemigroup.coe_infᵢ {M : Type u_2} [inst : Add M] {ι : Sort u_1} {S : ι → AddSubsemigroup M} : ↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

ink

@[simp]

theorem Subsemigroup.coe_infᵢ {M : Type u_2} [inst : Mul M] {ι : Sort u_1} {S : ι → Subsemigroup M} : ↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_14 {M : Type u_1} [inst : Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) : a ∈ s → infₛ s ≤ a

Equations

• (_ : ∀ (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M), a ∈ s → infₛ s ≤ a) = (_ : ∀ (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M), a ∈ s → infₛ s ≤ a)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] : ∀ (x : Set (AddSubsemigroup M)), IsGLB x (infₛ x)

Equations

• (_ : IsGLB x (infₛ x)) = (_ : IsGLB x (infₛ x))

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_2 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) : a ≤ a

Equations

• (_ : ∀ (a : AddSubsemigroup M), a ≤ a) = (_ : ∀ (a : AddSubsemigroup M), a ≤ a)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_9 {M : Type u_1} [inst : Add M] : ∀ (x x_1 : AddSubsemigroup M) (x_2 : M), x_2 ∈ ↑x ∧ x_2 ∈ ↑x_1 → x_2 ∈ ↑x

Equations

• (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x)

ink

instance AddSubsemigroup.instCompleteLatticeSubsemigroup {M : Type u_1} [inst : Add M] : CompleteLattice (AddSubsemigroup M)

The AddSubsemigroups of an AddMonoid form a complete lattice.

Equations

• One or more equations did not get rendered due to their size.

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_13 {M : Type u_1} [inst : Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) : (∀ (b : AddSubsemigroup M), b ∈ s → b ≤ a) → supₛ s ≤ a

Equations

• One or more equations did not get rendered due to their size.

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_5 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : AddSubsemigroup M), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : AddSubsemigroup M), a ≤ b → b ≤ a → a = b)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_10 {M : Type u_1} [inst : Add M] : ∀ (x x_1 : AddSubsemigroup M) (x_2 : M), x_2 ∈ ↑x ∧ x_2 ∈ ↑x_1 → x_2 ∈ ↑x_1

Equations

• (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_8 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) (c : AddSubsemigroup M) : a ≤ c → b ≤ c → a ⊔ b ≤ c

Equations

• (_ : ∀ (a b c : AddSubsemigroup M), a ≤ c → b ≤ c → a ⊔ b ≤ c) = (_ : ∀ (a b c : AddSubsemigroup M), a ≤ c → b ≤ c → a ⊔ b ≤ c)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_11 {M : Type u_1} [inst : Add M] : ∀ (x x_1 x_2 : AddSubsemigroup M), x ≤ x_1 → x ≤ x_2 → ∀ (x_3 : M), x_3 ∈ x → x_3 ∈ ↑x_1 ∧ x_3 ∈ ↑x_2

Equations

• (_ : x ∈ ↑x ∧ x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_7 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) : b ≤ a ⊔ b

Equations

• (_ : ∀ (a b : AddSubsemigroup M), b ≤ a ⊔ b) = (_ : ∀ (a b : AddSubsemigroup M), b ≤ a ⊔ b)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_17 {M : Type u_1} [inst : Add M] : ∀ (x : AddSubsemigroup M) (x_1 : M), x_1 ∈ ⊥ → x_1 ∈ x

Equations

• (_ : x ∈ x) = (_ : x ∈ x)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_4 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) : a < b ↔ a ≤ b ∧ ¬b ≤ a

Equations

• (_ : ∀ (a b : AddSubsemigroup M), a < b ↔ a ≤ b ∧ ¬b ≤ a) = (_ : ∀ (a b : AddSubsemigroup M), a < b ↔ a ≤ b ∧ ¬b ≤ a)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_15 {M : Type u_1} [inst : Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) : (∀ (b : AddSubsemigroup M), b ∈ s → a ≤ b) → a ≤ infₛ s

Equations

• One or more equations did not get rendered due to their size.

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_16 {M : Type u_1} [inst : Add M] : ∀ (x : AddSubsemigroup M) (x_1 : M), x_1 ∈ x → x_1 ∈ ⊤

Equations

• (_ : x ∈ ⊤) = (_ : x ∈ ⊤)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_6 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) : a ≤ a ⊔ b

Equations

• (_ : ∀ (a b : AddSubsemigroup M), a ≤ a ⊔ b) = (_ : ∀ (a b : AddSubsemigroup M), a ≤ a ⊔ b)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_12 {M : Type u_1} [inst : Add M] (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M) : a ∈ s → a ≤ supₛ s

Equations

• (_ : ∀ (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M), a ∈ s → a ≤ supₛ s) = (_ : ∀ (s : Set (AddSubsemigroup M)) (a : AddSubsemigroup M), a ∈ s → a ≤ supₛ s)

ink

def AddSubsemigroup.instCompleteLatticeSubsemigroup.proof_3 {M : Type u_1} [inst : Add M] (a : AddSubsemigroup M) (b : AddSubsemigroup M) (c : AddSubsemigroup M) : a ≤ b → b ≤ c → a ≤ c

Equations

• (_ : ∀ (a b c : AddSubsemigroup M), a ≤ b → b ≤ c → a ≤ c) = (_ : ∀ (a b c : AddSubsemigroup M), a ≤ b → b ≤ c → a ≤ c)

ink

instance Subsemigroup.instCompleteLatticeSubsemigroup {M : Type u_1} [inst : Mul M] : CompleteLattice (Subsemigroup M)

subsemigroups of a monoid form a complete lattice.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem AddSubsemigroup.subsingleton_of_subsingleton {M : Type u_1} [inst : Add M] [inst : Subsingleton (AddSubsemigroup M)] : Subsingleton M

ink

@[simp]

theorem Subsemigroup.subsingleton_of_subsingleton {M : Type u_1} [inst : Mul M] [inst : Subsingleton (Subsemigroup M)] : Subsingleton M

ink

instance AddSubsemigroup.instNontrivialSubsemigroup {M : Type u_1} [inst : Add M] [hn : Nonempty M] : Nontrivial (AddSubsemigroup M)

Equations

• @AddSubsemigroup.instNontrivialSubsemigroup = @AddSubsemigroup.instNontrivialSubsemigroup.proof_1

ink

def AddSubsemigroup.instNontrivialSubsemigroup.proof_1 {M : Type u_1} [inst : Add M] [hn : Nonempty M] : Nontrivial (AddSubsemigroup M)

Equations

• (_ : Nontrivial (AddSubsemigroup M)) = (_ : Nontrivial (AddSubsemigroup M))

ink

instance Subsemigroup.instNontrivialSubsemigroup {M : Type u_1} [inst : Mul M] [hn : Nonempty M] : Nontrivial (Subsemigroup M)

Equations

• @Subsemigroup.instNontrivialSubsemigroup = @Subsemigroup.instNontrivialSubsemigroup.proof_1

ink

def AddSubsemigroup.closure {M : Type u_1} [inst : Add M] (s : Set M) : AddSubsemigroup M

The AddSubsemigroup generated by a set

Equations

• AddSubsemigroup.closure s = infₛ { S | s ⊆ ↑S }

ink

def Subsemigroup.closure {M : Type u_1} [inst : Mul M] (s : Set M) : Subsemigroup M

The Subsemigroup generated by a set.

Equations

• Subsemigroup.closure s = infₛ { S | s ⊆ ↑S }

ink

theorem AddSubsemigroup.mem_closure {M : Type u_1} [inst : Add M] {s : Set M} {x : M} : x ∈ AddSubsemigroup.closure s ↔ ∀ (S : AddSubsemigroup M), s ⊆ ↑S → x ∈ S

ink

theorem Subsemigroup.mem_closure {M : Type u_1} [inst : Mul M] {s : Set M} {x : M} : x ∈ Subsemigroup.closure s ↔ ∀ (S : Subsemigroup M), s ⊆ ↑S → x ∈ S

ink

@[simp]

theorem AddSubsemigroup.subset_closure {M : Type u_1} [inst : Add M] {s : Set M} : s ⊆ ↑(AddSubsemigroup.closure s)

The AddSubsemigroup generated by a set includes the set.

ink

@[simp]

theorem Subsemigroup.subset_closure {M : Type u_1} [inst : Mul M] {s : Set M} : s ⊆ ↑(Subsemigroup.closure s)

The subsemigroup generated by a set includes the set.

ink

theorem AddSubsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [inst : Add M] {s : Set M} {P : M} (hP : ¬P ∈ AddSubsemigroup.closure s) : ¬P ∈ s

ink

theorem Subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [inst : Mul M] {s : Set M} {P : M} (hP : ¬P ∈ Subsemigroup.closure s) : ¬P ∈ s

ink

@[simp]

theorem AddSubsemigroup.closure_le {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M} : AddSubsemigroup.closure s ≤ S ↔ s ⊆ ↑S

An additive subsemigroup S includes closure s if and only if it includes s

ink

@[simp]

theorem Subsemigroup.closure_le {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M} : Subsemigroup.closure s ≤ S ↔ s ⊆ ↑S

A subsemigroup S includes closure s if and only if it includes s.

ink

theorem AddSubsemigroup.closure_mono {M : Type u_1} [inst : Add M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) : AddSubsemigroup.closure s ≤ AddSubsemigroup.closure t

Additive subsemigroup closure of a set is monotone in its argument: if s ⊆ t⊆ t, then closure s ≤ closure t≤ closure t

ink

theorem Subsemigroup.closure_mono {M : Type u_1} [inst : Mul M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) : Subsemigroup.closure s ≤ Subsemigroup.closure t

subsemigroup closure of a set is monotone in its argument: if s ⊆ t⊆ t, then closure s ≤ closure t≤ closure t.

ink

theorem AddSubsemigroup.closure_eq_of_le {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ AddSubsemigroup.closure s) : AddSubsemigroup.closure s = S

ink

theorem Subsemigroup.closure_eq_of_le {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ Subsemigroup.closure s) : Subsemigroup.closure s = S

ink

theorem AddSubsemigroup.closure_induction {M : Type u_1} [inst : Add M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ AddSubsemigroup.closure s) (Hs : (x : M) → x ∈ s → p x) (Hmul : (x y : M) → p x → p y → p (x + y)) : p x

An induction principle for additive closure membership. If p holds for all elements of s, and is preserved under addition, then p holds for all elements of the additive closure of s.

ink

theorem Subsemigroup.closure_induction {M : Type u_1} [inst : Mul M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ Subsemigroup.closure s) (Hs : (x : M) → x ∈ s → p x) (Hmul : (x y : M) → p x → p y → p (x * y)) : p x

An induction principle for closure membership. If p holds for all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

ink

theorem AddSubsemigroup.closure_induction' {M : Type u_1} [inst : Add M] (s : Set M) {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop} (Hs : (x : M) → (h : x ∈ s) → p x (_ : x ∈ ↑(AddSubsemigroup.closure s))) (Hmul : (x : M) → (hx : x ∈ AddSubsemigroup.closure s) → (y : M) → (hy : y ∈ AddSubsemigroup.closure s) → p x hx → p y hy → p (x + y) (_ : x + y ∈ AddSubsemigroup.closure s)) {x : M} (hx : x ∈ AddSubsemigroup.closure s) : p x hx

A dependent version of AddSubsemigroup.closure_induction.

ink

abbrev AddSubsemigroup.closure_induction'.match_1 {M : Type u_1} [inst : Add M] (s : Set M) {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop} (y : M) (motive : (∃ x, p y x) → Prop) : (x : ∃ x, p y x) → ((hy' : y ∈ AddSubsemigroup.closure s) → (hy : p y hy') → motive (_ : ∃ x, p y x)) → motive x

Equations

• AddSubsemigroup.closure_induction'.match_1 s y motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

theorem Subsemigroup.closure_induction' {M : Type u_1} [inst : Mul M] (s : Set M) {p : (x : M) → x ∈ Subsemigroup.closure s → Prop} (Hs : (x : M) → (h : x ∈ s) → p x (_ : x ∈ ↑(Subsemigroup.closure s))) (Hmul : (x : M) → (hx : x ∈ Subsemigroup.closure s) → (y : M) → (hy : y ∈ Subsemigroup.closure s) → p x hx → p y hy → p (x * y) (_ : x * y ∈ Subsemigroup.closure s)) {x : M} (hx : x ∈ Subsemigroup.closure s) : p x hx

A dependent version of Subsemigroup.closure_induction.

ink

theorem AddSubsemigroup.closure_induction₂ {M : Type u_1} [inst : Add M] {s : Set M} {p : M → M → Prop} {x : M} {y : M} (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) (Hs : (x : M) → x ∈ s → (y : M) → y ∈ s → p x y) (Hmul_left : (x y z : M) → p x z → p y z → p (x + y) z) (Hmul_right : (x y z : M) → p z x → p z y → p z (x + y)) : p x y

An induction principle for additive closure membership for predicates with two arguments.

ink

theorem Subsemigroup.closure_induction₂ {M : Type u_1} [inst : Mul M] {s : Set M} {p : M → M → Prop} {x : M} {y : M} (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s) (Hs : (x : M) → x ∈ s → (y : M) → y ∈ s → p x y) (Hmul_left : (x y z : M) → p x z → p y z → p (x * y) z) (Hmul_right : (x y z : M) → p z x → p z y → p z (x * y)) : p x y

An induction principle for closure membership for predicates with two arguments.

ink

theorem AddSubsemigroup.dense_induction {M : Type u_1} [inst : Add M] {p : M → Prop} (x : M) {s : Set M} (hs : AddSubsemigroup.closure s = ⊤) (Hs : (x : M) → x ∈ s → p x) (Hmul : (x y : M) → p x → p y → p (x + y)) : p x

If s is a dense set in an additive monoid M, AddSubsemigroup.closure s = ⊤⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s∈ s, and verify that p x and p y imply p (x + y).

ink

theorem Subsemigroup.dense_induction {M : Type u_1} [inst : Mul M] {p : M → Prop} (x : M) {s : Set M} (hs : Subsemigroup.closure s = ⊤) (Hs : (x : M) → x ∈ s → p x) (Hmul : (x y : M) → p x → p y → p (x * y)) : p x

If s is a dense set in a magma M, Subsemigroup.closure s = ⊤⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s∈ s, and verify that p x and p y imply p (x * y).

ink

def AddSubsemigroup.gi.proof_2 (M : Type u_1) [inst : Add M] : ∀ (x : AddSubsemigroup M), ↑x ⊆ ↑(AddSubsemigroup.closure ↑x)

Equations

• (_ : ↑x ⊆ ↑(AddSubsemigroup.closure ↑x)) = (_ : ↑x ⊆ ↑(AddSubsemigroup.closure ↑x))

ink

def AddSubsemigroup.gi.proof_1 (M : Type u_1) [inst : Add M] : ∀ (x : Set M) (x_1 : AddSubsemigroup M), AddSubsemigroup.closure x ≤ x_1 ↔ x ⊆ ↑x_1

Equations

• (_ : AddSubsemigroup.closure x ≤ x ↔ x ⊆ ↑x) = (_ : AddSubsemigroup.closure x ≤ x ↔ x ⊆ ↑x)

ink

def AddSubsemigroup.gi (M : Type u_1) [inst : Add M] : GaloisInsertion AddSubsemigroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• One or more equations did not get rendered due to their size.

ink

def Subsemigroup.gi (M : Type u_1) [inst : Mul M] : GaloisInsertion Subsemigroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem AddSubsemigroup.closure_eq {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) : AddSubsemigroup.closure ↑S = S

Additive closure of an additive subsemigroup S equals S

ink

@[simp]

theorem Subsemigroup.closure_eq {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) : Subsemigroup.closure ↑S = S

Closure of a subsemigroup S equals S.

ink

@[simp]

theorem AddSubsemigroup.closure_empty {M : Type u_1} [inst : Add M] : AddSubsemigroup.closure ∅ = ⊥

ink

@[simp]

theorem Subsemigroup.closure_empty {M : Type u_1} [inst : Mul M] : Subsemigroup.closure ∅ = ⊥

ink

@[simp]

theorem AddSubsemigroup.closure_univ {M : Type u_1} [inst : Add M] : AddSubsemigroup.closure Set.univ = ⊤

ink

@[simp]

theorem Subsemigroup.closure_univ {M : Type u_1} [inst : Mul M] : Subsemigroup.closure Set.univ = ⊤

ink

theorem AddSubsemigroup.closure_union {M : Type u_1} [inst : Add M] (s : Set M) (t : Set M) : AddSubsemigroup.closure (s ∪ t) = AddSubsemigroup.closure s ⊔ AddSubsemigroup.closure t

ink

theorem Subsemigroup.closure_union {M : Type u_1} [inst : Mul M] (s : Set M) (t : Set M) : Subsemigroup.closure (s ∪ t) = Subsemigroup.closure s ⊔ Subsemigroup.closure t

ink

theorem AddSubsemigroup.closure_unionᵢ {M : Type u_2} [inst : Add M] {ι : Sort u_1} (s : ι → Set M) : AddSubsemigroup.closure (Set.unionᵢ fun i => s i) = ⨆ i, AddSubsemigroup.closure (s i)

ink

theorem Subsemigroup.closure_unionᵢ {M : Type u_2} [inst : Mul M] {ι : Sort u_1} (s : ι → Set M) : Subsemigroup.closure (Set.unionᵢ fun i => s i) = ⨆ i, Subsemigroup.closure (s i)

ink

theorem AddSubsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [inst : Add M] (m : M) (p : AddSubsemigroup M) : AddSubsemigroup.closure {m} ≤ p ↔ m ∈ p

ink

theorem Subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [inst : Mul M] (m : M) (p : Subsemigroup M) : Subsemigroup.closure {m} ≤ p ↔ m ∈ p

ink

theorem AddSubsemigroup.mem_supᵢ {M : Type u_2} [inst : Add M] {ι : Sort u_1} (p : ι → AddSubsemigroup M) {m : M} : (m ∈ ⨆ i, p i) ↔ ∀ (N : AddSubsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

ink

theorem Subsemigroup.mem_supᵢ {M : Type u_2} [inst : Mul M] {ι : Sort u_1} (p : ι → Subsemigroup M) {m : M} : (m ∈ ⨆ i, p i) ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

ink

theorem AddSubsemigroup.supᵢ_eq_closure {M : Type u_2} [inst : Add M] {ι : Sort u_1} (p : ι → AddSubsemigroup M) : (⨆ i, p i) = AddSubsemigroup.closure (Set.unionᵢ fun i => ↑(p i))

ink

theorem Subsemigroup.supᵢ_eq_closure {M : Type u_2} [inst : Mul M] {ι : Sort u_1} (p : ι → Subsemigroup M) : (⨆ i, p i) = Subsemigroup.closure (Set.unionᵢ fun i => ↑(p i))

ink

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

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

Equations

• AddHom.eqLocus f g = { carrier := { x | ↑f x = ↑g x }, add_mem' := (_ : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a + b) = ↑g (a + b)) }

ink

def AddHom.eqLocus.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (g : AddHom M N) : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a + b) = ↑g (a + b)

Equations

• (_ : ↑f (a + b) = ↑g (a + b)) = (_ : ↑f (a + b) = ↑g (a + b))

ink

def MulHom.eqLocus {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (g : M →ₙ* N) : Subsemigroup M

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

Equations

• MulHom.eqLocus f g = { carrier := { x | ↑f x = ↑g x }, mul_mem' := (_ : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a * b) = ↑g (a * b)) }

ink

theorem AddHom.eqOn_closure {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {g : AddHom M N} {s : Set M} (h : Set.EqOn (↑f) (↑g) s) : Set.EqOn ↑f ↑g ↑(AddSubsemigroup.closure s)

If two add homomorphisms are equal on a set, then they are equal on its additive subsemigroup closure.

ink

theorem MulHom.eqOn_closure {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {g : M →ₙ* N} {s : Set M} (h : Set.EqOn (↑f) (↑g) s) : Set.EqOn ↑f ↑g ↑(Subsemigroup.closure s)

If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure.

ink

theorem AddHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn ↑f ↑g ↑⊤) : f = g

ink

theorem MulHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn ↑f ↑g ↑⊤) : f = g

ink

theorem AddHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {s : Set M} (hs : AddSubsemigroup.closure s = ⊤) {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn (↑f) (↑g) s) : f = g

ink

theorem MulHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {s : Set M} (hs : Subsemigroup.closure s = ⊤) {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn (↑f) (↑g) s) : f = g

ink

def AddHom.ofDense {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst : AddSemigroup N] {s : Set M} (f : M → N) (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) : AddHom M N

Let s be a subset of an additive semigroup M such that the closure of s is the whole semigroup. Then AddHom.ofDense defines an additive homomorphism from M asking for a proof of f (x + y) = f x + f y only for y ∈ s∈ s.

Equations

• AddHom.ofDense f hs hmul = { toFun := f, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }

ink

def AddHom.ofDense.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddSemigroup M] [inst : AddSemigroup N] {s : Set M} (f : M → N) (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) (x : M) (y : M) : f (x + y) = f x + f y

Equations

• (_ : f (x + y) = f x + f y) = (_ : f (x + y) = f x + f y)

ink

def MulHom.ofDense {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst : Semigroup N] {s : Set M} (f : M → N) (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) : M →ₙ* N

Let s be a subset of a semigroup M such that the closure of s is the whole semigroup. Then MulHom.ofDense defines a mul homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s∈ s.

Equations

• MulHom.ofDense f hs hmul = { toFun := f, map_mul' := (_ : ∀ (x y : M), f (x * y) = f x * f y) }

ink

@[simp]

theorem AddHom.coe_ofDense {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst : AddSemigroup N] {s : Set M} (f : M → N) (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) : ↑(AddHom.ofDense f hs hmul) = f

ink

@[simp]

theorem MulHom.coe_ofDense {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst : Semigroup N] {s : Set M} (f : M → N) (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) : ↑(MulHom.ofDense f hs hmul) = f