Non-unital Subalgebras over Commutative Semirings

In this file we define NonUnitalSubalgebras and the usual operations on them (map, comap).

TODO

• once we have scalar actions by semigroups (as opposed to monoids), implement the action of a non-unital subalgebra on the larger algebra.

def NonUnitalSubalgebraClass.subtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : { x // x ∈ s } →ₙₐ[R] A

Embedding of a non-unital subalgebra into the non-unital algebra.

@[simp]

theorem NonUnitalSubalgebraClass.coeSubtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : ↑(NonUnitalSubalgebraClass.subtype s) = Subtype.val

structure NonUnitalSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] extends NonUnitalSubsemiring : Type v

• carrier : Set A
• add_mem' : ∀ {a b : A}, a ∈ s.carrier → b ∈ s.carrier → a + b ∈ s.carrier
• zero_mem' : 0 ∈ s.carrier
• mul_mem' : ∀ {a b : A}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
• smul_mem' : ∀ (c : R) {x : A}, x ∈ s.carrier → c • x ∈ s.carrier

  The carrier set is closed under scalar multiplication.

A non-unital subalgebra is a sub(semi)ring that is also a submodule.

@[reducible]

abbrev NonUnitalSubalgebra.toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) : Submodule R A

Reinterpret a NonUnitalSubalgebra as a Submodule.

instance NonUnitalSubalgebra.instSetLikeNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SetLike (NonUnitalSubalgebra R A) A

instance NonUnitalSubalgebra.instNonUnitalSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A

instance NonUnitalSubalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SMulMemClass (NonUnitalSubalgebra R A) R A

instance NonUnitalSubalgebra.instNonUnitalSubringClass {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] : NonUnitalSubringClass (NonUnitalSubalgebra R A) A

theorem NonUnitalSubalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s : NonUnitalSubalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s

theorem NonUnitalSubalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) : S = T

@[simp]

theorem NonUnitalSubalgebra.mem_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toNonUnitalSubsemiring = ↑S

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} : S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring ↔ S = U

theorem NonUnitalSubalgebra.mem_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) {x : A} : x ∈ NonUnitalSubalgebra.toSubmodule S ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑(NonUnitalSubalgebra.toSubmodule S) = ↑S

theorem NonUnitalSubalgebra.toSubmodule_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective NonUnitalSubalgebra.toSubmodule

theorem NonUnitalSubalgebra.toSubmodule_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.toSubmodule S = NonUnitalSubalgebra.toSubmodule U ↔ S = U

def NonUnitalSubalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : NonUnitalSubalgebra R A

Copy of a non-unital subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem NonUnitalSubalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : ↑(NonUnitalSubalgebra.copy S s hs) = s

theorem NonUnitalSubalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : NonUnitalSubalgebra.copy S s hs = S

def NonUnitalSubalgebra.toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubring A

A non-unital subalgebra over a ring is also a Subring.

@[simp]

theorem NonUnitalSubalgebra.mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ NonUnitalSubalgebra.toNonUnitalSubring S ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑(NonUnitalSubalgebra.toNonUnitalSubring S) = ↑S

theorem NonUnitalSubalgebra.toNonUnitalSubring_injective {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] : Function.Injective NonUnitalSubalgebra.toNonUnitalSubring

theorem NonUnitalSubalgebra.toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] {S : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.toNonUnitalSubring S = NonUnitalSubalgebra.toNonUnitalSubring U ↔ S = U

instance NonUnitalSubalgebra.instInhabitedSubtypeMemNonUnitalSubalgebraInstMembershipInstSetLikeNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : Inhabited { x // x ∈ S }

NonUnitalSubalgebras inherit structure from their NonUnitalSubsemiring / Semiring coercions.

instance NonUnitalSubalgebra.toNonUnitalSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSemiring { x // x ∈ S }

instance NonUnitalSubalgebra.toNonUnitalCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommSemiring { x // x ∈ S }

instance NonUnitalSubalgebra.toNonUnitalRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalRing { x // x ∈ S }

instance NonUnitalSubalgebra.toNonUnitalCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalCommRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommRing { x // x ∈ S }

def NonUnitalSubalgebra.toSubmodule' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o Submodule R A

The forgetful map from NonUnitalSubalgebra to Submodule as an OrderEmbedding

def NonUnitalSubalgebra.toNonUnitalSubsemiring' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubsemiring A

The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

def NonUnitalSubalgebra.toNonUnitalSubring' {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubring A

The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

NonUnitalSubalgebras inherit structure from their Submodule coercions.

instance NonUnitalSubalgebra.instModule' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : Module R' { x // x ∈ S }

instance NonUnitalSubalgebra.instModule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : Module R { x // x ∈ S }

instance NonUnitalSubalgebra.instIsScalarTower' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R { x // x ∈ S }

instance NonUnitalSubalgebra.instIsScalarTowerSubtypeMemNonUnitalSubalgebraInstMembershipInstSetLikeNonUnitalSubalgebraToSMulZeroToAddZeroClassToAddMonoidToAddCommMonoidToAddSubmonoidToNonUnitalSubsemiringToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToAddCommMonoidInstModuleToSMulToSMulZeroClassToSMulWithZeroToMulZeroClassToNonUnitalNonAssocSemiringInstNonUnitalSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [IsScalarTower R A A] : IsScalarTower R { x // x ∈ S } { x // x ∈ S }

instance NonUnitalSubalgebra.instSMulCommClass' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SMulCommClass R' R A] : SMulCommClass R' R { x // x ∈ S }

instance NonUnitalSubalgebra.instSMulCommClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [SMulCommClass R A A] : SMulCommClass R { x // x ∈ S } { x // x ∈ S }

instance NonUnitalSubalgebra.noZeroSMulDivisors_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R { x // x ∈ S }

theorem NonUnitalSubalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (x : { x // x ∈ S }) (y : { x // x ∈ S }) : ↑(x + y) = ↑x + ↑y

theorem NonUnitalSubalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (x : { x // x ∈ S }) (y : { x // x ∈ S }) : ↑(x * y) = ↑x * ↑y

theorem NonUnitalSubalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑0 = 0

theorem NonUnitalSubalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x : { x // x ∈ S }) : ↑(-x) = -↑x

theorem NonUnitalSubalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x : { x // x ∈ S }) (y : { x // x ∈ S }) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem NonUnitalSubalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : { x // x ∈ S }) : ↑(r • x) = r • ↑x

theorem NonUnitalSubalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) {x : { x // x ∈ S }} : ↑x = 0 ↔ x = 0

@[simp]

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)

@[simp]

theorem NonUnitalSubalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)

def NonUnitalSubalgebra.toSubmoduleEquiv {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : { x // x ∈ NonUnitalSubalgebra.toSubmodule S } ≃ₗ[R] { x // x ∈ S }

Linear equivalence between S : Submodule R A and S. Though these types are equal, we define it as a LinearEquiv to avoid type equalities.

def NonUnitalSubalgebra.map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R B

Transport a non-unital subalgebra via an algebra homomorphism.

theorem NonUnitalSubalgebra.map_mono {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.map f S₂

theorem NonUnitalSubalgebra.map_injective {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ↑f) : Function.Injective (NonUnitalSubalgebra.map f)

@[simp]

theorem NonUnitalSubalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map (NonUnitalAlgHom.id R A) S = S

theorem NonUnitalSubalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalNonAssocSemiring C] [Module R C] (S : NonUnitalSubalgebra R A) (g : B →ₙₐ[R] C) (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map g (NonUnitalSubalgebra.map f S) = NonUnitalSubalgebra.map (NonUnitalAlgHom.comp g f) S

@[simp]

theorem NonUnitalSubalgebra.mem_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalSubalgebra.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

theorem NonUnitalSubalgebra.map_toSubmodule {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : NonUnitalSubalgebra.toSubmodule (NonUnitalSubalgebra.map f S) = Submodule.map (↑↑f) (NonUnitalSubalgebra.toSubmodule S)

theorem NonUnitalSubalgebra.map_toNonUnitalSubsemiring {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring

@[simp]

theorem NonUnitalSubalgebra.coe_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F) : ↑(NonUnitalSubalgebra.map f S) = ↑f '' ↑S

def NonUnitalSubalgebra.comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R A

Preimage of a non-unital subalgebra under an algebra homomorphism.

theorem NonUnitalSubalgebra.map_le {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {U : NonUnitalSubalgebra R B} : NonUnitalSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalSubalgebra.comap f U

theorem NonUnitalSubalgebra.gc_map_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) : GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)

@[simp]

theorem NonUnitalSubalgebra.mem_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A) : x ∈ NonUnitalSubalgebra.comap f S ↔ ↑f x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) : ↑(NonUnitalSubalgebra.comap f S) = ↑f ⁻¹' ↑S

instance NonUnitalSubalgebra.noZeroDivisors {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] (S : NonUnitalSubalgebra R A) : NoZeroDivisors { x // x ∈ S }

def Submodule.toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : NonUnitalSubalgebra R A

A submodule closed under multiplication is a non-unital subalgebra.

@[simp]

theorem Submodule.mem_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {p : Submodule R A} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A} : x ∈ Submodule.toNonUnitalSubalgebra p h_mul ↔ x ∈ p

@[simp]

theorem Submodule.coe_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : ↑(Submodule.toNonUnitalSubalgebra p h_mul) = ↑p

theorem Submodule.toNonUnitalSubalgebra_mk {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (hmul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : Submodule.toNonUnitalSubalgebra p hmul = { toNonUnitalSubsemiring := { toAddSubmonoid := { toAddSubsemigroup := { carrier := ↑p, add_mem' := (_ : ∀ {a b : A}, a ∈ p → b ∈ p → a + b ∈ p) }, zero_mem' := (_ : 0 ∈ p) }, mul_mem' := fun {a b} => hmul a b }, smul_mem' := (_ : ∀ (c : R) {x : A}, x ∈ p.carrier → c • x ∈ p.carrier) }

@[simp]

theorem Submodule.toNonUnitalSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : NonUnitalSubalgebra.toSubmodule (Submodule.toNonUnitalSubalgebra p h_mul) = p

@[simp]

theorem NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : Submodule.toNonUnitalSubalgebra (NonUnitalSubalgebra.toSubmodule S) (_ : ∀ (x x_1 : A), x ∈ S → x_1 ∈ S → x * x_1 ∈ S) = S

def NonUnitalAlgHom.range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (φ : F) : NonUnitalSubalgebra R B

Range of an NonUnitalAlgHom as a non-unital subalgebra.

@[simp]

theorem NonUnitalAlgHom.mem_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (φ : F) {y : B} : y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, ↑φ x = y

theorem NonUnitalAlgHom.mem_range_self {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (φ : F) (x : A) : ↑φ x ∈ NonUnitalAlgHom.range φ

@[simp]

theorem NonUnitalAlgHom.coe_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (φ : F) : ↑(NonUnitalAlgHom.range φ) = Set.range ↑φ

theorem NonUnitalAlgHom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalNonAssocSemiring C] [Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : NonUnitalAlgHom.range (NonUnitalAlgHom.comp g f) = NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f)

theorem NonUnitalAlgHom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalNonAssocSemiring C] [Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : NonUnitalAlgHom.range (NonUnitalAlgHom.comp g f) ≤ NonUnitalAlgHom.range g

def NonUnitalAlgHom.codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), ↑f x ∈ S) : A →ₙₐ[R] { x // x ∈ S }

Restrict the codomain of a non-unital algebra homomorphism.

@[simp]

theorem NonUnitalAlgHom.subtype_comp_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), ↑f x ∈ S) : NonUnitalAlgHom.comp (NonUnitalSubalgebraClass.subtype S) (NonUnitalAlgHom.codRestrict f S hf) = ↑f

@[simp]

theorem NonUnitalAlgHom.coe_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), ↑f x ∈ S) (x : A) : ↑(↑(NonUnitalAlgHom.codRestrict f S hf) x) = ↑f x

theorem NonUnitalAlgHom.injective_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), ↑f x ∈ S) : Function.Injective ↑(NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective ↑f

@[reducible]

def NonUnitalAlgHom.rangeRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] { x // x ∈ NonUnitalAlgHom.range f }

Restrict the codomain of an NonUnitalAlgHom f to f.range.

This is the bundled version of Set.rangeFactorization.

def NonUnitalAlgHom.equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (ϕ : F) (ψ : F) : NonUnitalSubalgebra R A

The equalizer of two non-unital R-algebra homomorphisms

@[simp]

theorem NonUnitalAlgHom.mem_equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] (φ : F) (ψ : F) (x : A) : x ∈ NonUnitalAlgHom.equalizer φ ψ ↔ ↑φ x = ↑ψ x

instance NonUnitalAlgHom.fintypeRange {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalAlgHomClass F R A B] [Fintype A] [DecidableEq B] (φ : F) : Fintype { x // x ∈ NonUnitalAlgHom.range φ }

The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with Subtype.fintype if B is also a fintype.

def NonUnitalAlgebra.adjoin (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalSubalgebra R A

The minimal non-unital subalgebra that includes s.

theorem NonUnitalAlgebra.adjoin_toSubmodule (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.adjoin R s) = Submodule.span R ↑(NonUnitalSubsemiring.closure s)

theorem NonUnitalAlgebra.subset_adjoin (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} : s ⊆ ↑(NonUnitalAlgebra.adjoin R s)

theorem NonUnitalAlgebra.self_mem_adjoin_singleton (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : A) : x ∈ NonUnitalAlgebra.adjoin R {x}

theorem NonUnitalAlgebra.adjoin_induction {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : A → Prop} {a : A} (h : a ∈ NonUnitalAlgebra.adjoin R s) (Hs : (x : A) → x ∈ s → p x) (Hadd : (x y : A) → p x → p y → p (x + y)) (H0 : p 0) (Hmul : (x y : A) → p x → p y → p (x * y)) (Hsmul : (r : R) → (x : A) → p x → p (r • x)) : p a

If some predicate holds for all x ∈ (s : Set A) and this predicate is closed under the algebraMap, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

theorem NonUnitalAlgebra.adjoin_induction₂ {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : A → A → Prop} {a : A} {b : A} (ha : a ∈ NonUnitalAlgebra.adjoin R s) (hb : b ∈ NonUnitalAlgebra.adjoin R s) (Hs : (x : A) → x ∈ s → (y : A) → y ∈ s → p x y) (H0_left : (y : A) → p 0 y) (H0_right : (x : A) → p x 0) (Hadd_left : (x₁ x₂ y : A) → p x₁ y → p x₂ y → p (x₁ + x₂) y) (Hadd_right : (x y₁ y₂ : A) → p x y₁ → p x y₂ → p x (y₁ + y₂)) (Hmul_left : (x₁ x₂ y : A) → p x₁ y → p x₂ y → p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : A) → p x y₁ → p x y₂ → p x (y₁ * y₂)) (Hsmul_left : (r : R) → (x y : A) → p x y → p (r • x) y) (Hsmul_right : (r : R) → (x y : A) → p x y → p x (r • y)) : p a b

theorem NonUnitalAlgebra.adjoin_induction' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : { x // x ∈ NonUnitalAlgebra.adjoin R s } → Prop} (a : { x // x ∈ NonUnitalAlgebra.adjoin R s }) (Hs : (x : A) → (h : x ∈ s) → p { val := x, property := (_ : x ∈ ↑(NonUnitalAlgebra.adjoin R s)) }) (Hadd : (x y : { x // x ∈ NonUnitalAlgebra.adjoin R s }) → p x → p y → p (x + y)) (H0 : p 0) (Hmul : (x y : { x // x ∈ NonUnitalAlgebra.adjoin R s }) → p x → p y → p (x * y)) (Hsmul : (r : R) → (x : { x // x ∈ NonUnitalAlgebra.adjoin R s }) → p x → p (r • x)) : p a

The difference with NonUnitalAlgebra.adjoin_induction is that this acts on the subtype.

theorem NonUnitalAlgebra.gc {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : GaloisConnection (NonUnitalAlgebra.adjoin R) SetLike.coe

def NonUnitalAlgebra.gi {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : GaloisInsertion (NonUnitalAlgebra.adjoin R) SetLike.coe

Galois insertion between adjoin and Subtype.val.

instance NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CompleteLattice (NonUnitalSubalgebra R A)

theorem NonUnitalAlgebra.adjoin_le {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {s : Set A} (hs : s ⊆ ↑S) : NonUnitalAlgebra.adjoin R s ≤ S

theorem NonUnitalAlgebra.adjoin_le_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {s : Set A} : NonUnitalAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S

theorem NonUnitalAlgebra.adjoin_union {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) (t : Set A) : NonUnitalAlgebra.adjoin R (s ∪ t) = NonUnitalAlgebra.adjoin R s ⊔ NonUnitalAlgebra.adjoin R t

@[simp]

theorem NonUnitalAlgebra.adjoin_empty (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalAlgebra.adjoin R ∅ = ⊥

@[simp]

theorem NonUnitalAlgebra.adjoin_univ (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalAlgebra.adjoin R Set.univ = ⊤

@[simp]

theorem NonUnitalAlgebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊤ = Set.univ

@[simp]

theorem NonUnitalAlgebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} : x ∈ ⊤

@[simp]

theorem NonUnitalAlgebra.top_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.toSubmodule ⊤ = ⊤

@[simp]

theorem NonUnitalAlgebra.top_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubsemiring = ⊤

@[simp]

theorem NonUnitalAlgebra.top_toSubring {R : Type u_2} {A : Type u_3} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.toNonUnitalSubring ⊤ = ⊤

@[simp]

theorem NonUnitalAlgebra.toSubmodule_eq_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.toSubmodule S = ⊤ ↔ S = ⊤

@[simp]

theorem NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

@[simp]

theorem NonUnitalAlgebra.to_subring_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.toNonUnitalSubring S = ⊤ ↔ S = ⊤

theorem NonUnitalAlgebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} : x ∈ S → x ∈ S ⊔ T

theorem NonUnitalAlgebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} : x ∈ T → x ∈ S ⊔ T

theorem NonUnitalAlgebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} {y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem NonUnitalAlgebra.map_sup {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T

@[simp]

theorem NonUnitalAlgebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) : ↑(S ⊓ T) = ↑S ∩ ↑T

@[simp]

theorem NonUnitalAlgebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

@[simp]

theorem NonUnitalAlgebra.inf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.toSubmodule (S ⊓ T) = NonUnitalSubalgebra.toSubmodule S ⊓ NonUnitalSubalgebra.toSubmodule T

@[simp]

theorem NonUnitalAlgebra.inf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) (T : NonUnitalSubalgebra R A) : (S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring

@[simp]

theorem NonUnitalAlgebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : ↑(sInf S) = ⋂ (s : NonUnitalSubalgebra R A) (_ : s ∈ S), ↑s

theorem NonUnitalAlgebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : Set (NonUnitalSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ (p : NonUnitalSubalgebra R A), p ∈ S → x ∈ p

@[simp]

theorem NonUnitalAlgebra.sInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : NonUnitalSubalgebra.toSubmodule (sInf S) = sInf (NonUnitalSubalgebra.toSubmodule '' S)

@[simp]

theorem NonUnitalAlgebra.sInf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)

@[simp]

theorem NonUnitalAlgebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

theorem NonUnitalAlgebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A} {x : A} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem NonUnitalAlgebra.iInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} (S : ι → NonUnitalSubalgebra R A) : NonUnitalSubalgebra.toSubmodule (⨅ (i : ι), S i) = ⨅ (i : ι), NonUnitalSubalgebra.toSubmodule (S i)

instance NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Inhabited (NonUnitalSubalgebra R A)

theorem NonUnitalAlgebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} : x ∈ ⊥ ↔ x = 0

theorem NonUnitalAlgebra.toSubmodule_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.toSubmodule ⊥ = ⊥

@[simp]

theorem NonUnitalAlgebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊥ = {0}

theorem NonUnitalAlgebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : S = ⊤ ↔ ∀ (x : A), x ∈ S

theorem NonUnitalAlgebra.range_top_iff_surjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalAlgHom.range f = ⊤ ↔ Function.Surjective ↑f

@[simp]

theorem NonUnitalAlgebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalAlgHom.range (NonUnitalAlgHom.id R A) = ⊤

@[simp]

theorem NonUnitalAlgebra.map_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊤ = NonUnitalAlgHom.range f

@[simp]

theorem NonUnitalAlgebra.map_bot {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊥ = ⊥

@[simp]

theorem NonUnitalAlgebra.comap_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.comap f ⊤ = ⊤

def NonUnitalAlgebra.toTop {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : A →ₙₐ[R] { x // x ∈ ⊤ }

NonUnitalAlgHom to ⊤ : NonUnitalSubalgebra R A.

instance NonUnitalSubalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Subsingleton A] : Subsingleton (NonUnitalSubalgebra R A)

instance NonUnitalAlgHom.subsingleton {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [Subsingleton (NonUnitalSubalgebra R A)] : Subsingleton (A →ₙₐ[R] B)

theorem NonUnitalSubalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S

def NonUnitalSubalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) : { x // x ∈ S } →ₙₐ[R] { x // x ∈ T }

The map S → T when S is a non-unital subalgebra contained in the non-unital subalgebra T.

This is the non-unital subalgebra version of Submodule.ofLe, or Subring.inclusion

theorem NonUnitalSubalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) : Function.Injective ↑(NonUnitalSubalgebra.inclusion h)

@[simp]

theorem NonUnitalSubalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.inclusion (_ : S ≤ S) = NonUnitalAlgHom.id R { x // x ∈ S }

@[simp]

theorem NonUnitalSubalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) : ↑(NonUnitalSubalgebra.inclusion h) { val := x, property := hx } = { val := x, property := h x hx }

theorem NonUnitalSubalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : { x // x ∈ T }) (m : ↑x ∈ S) : ↑(NonUnitalSubalgebra.inclusion h) { val := ↑x, property := m } = x

@[simp]

theorem NonUnitalSubalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : { x // x ∈ S }) : ↑(NonUnitalSubalgebra.inclusion htu) (↑(NonUnitalSubalgebra.inclusion hst) x) = ↑(NonUnitalSubalgebra.inclusion (_ : S ≤ U)) x

@[simp]

theorem NonUnitalSubalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : { x // x ∈ S }) : ↑(↑(NonUnitalSubalgebra.inclusion h) s) = ↑s

def NonUnitalSubalgebra.prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] (S : NonUnitalSubalgebra R A) (S₁ : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R (A × B)

The product of two non-unital subalgebras is a non-unital subalgebra.

@[simp]

theorem NonUnitalSubalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] (S : NonUnitalSubalgebra R A) (S₁ : NonUnitalSubalgebra R B) : ↑(NonUnitalSubalgebra.prod S S₁) = ↑S ×ˢ ↑S₁

theorem NonUnitalSubalgebra.prod_toSubmodule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] (S : NonUnitalSubalgebra R A) (S₁ : NonUnitalSubalgebra R B) : NonUnitalSubalgebra.toSubmodule (NonUnitalSubalgebra.prod S S₁) = Submodule.prod (NonUnitalSubalgebra.toSubmodule S) (NonUnitalSubalgebra.toSubmodule S₁)

@[simp]

theorem NonUnitalSubalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] {S : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {x : A × B} : x ∈ NonUnitalSubalgebra.prod S S₁ ↔ x.fst ∈ S ∧ x.snd ∈ S₁

@[simp]

theorem NonUnitalSubalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] : NonUnitalSubalgebra.prod ⊤ ⊤ = ⊤

theorem NonUnitalSubalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {T₁ : NonUnitalSubalgebra R B} : S ≤ T → S₁ ≤ T₁ → NonUnitalSubalgebra.prod S S₁ ≤ NonUnitalSubalgebra.prod T T₁

@[simp]

theorem NonUnitalSubalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {T₁ : NonUnitalSubalgebra R B} : NonUnitalSubalgebra.prod S S₁ ⊓ NonUnitalSubalgebra.prod T T₁ = NonUnitalSubalgebra.prod (S ⊓ T) (S₁ ⊓ T₁)

theorem NonUnitalSubalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Type u_1} [Nonempty ι] {S : ι → NonUnitalSubalgebra R A} (dir : Directed (fun x x_1 => x ≤ x_1) S) : ↑(iSup S) = ⋃ (i : ι), ↑(S i)

noncomputable def NonUnitalSubalgebra.iSupLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (dir : Directed (fun x x_1 => x ≤ x_1) K) (f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (NonUnitalSubalgebra.inclusion h)) (T : NonUnitalSubalgebra R A) (hT : T = iSup K) : { x // x ∈ T } →ₙₐ[R] B

Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining it on each non-unital subalgebra, and proving that it agrees on the intersection of non-unital subalgebras.

@[simp]

theorem NonUnitalSubalgebra.iSupLift_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x x_1 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x ∈ K i }) (h : K i ≤ T) : ↑(NonUnitalSubalgebra.iSupLift K dir f hf T hT) (↑(NonUnitalSubalgebra.inclusion h) x) = ↑(f i) x

@[simp]

theorem NonUnitalSubalgebra.iSupLift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x x_1 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) : NonUnitalAlgHom.comp (NonUnitalSubalgebra.iSupLift K dir f hf T hT) (NonUnitalSubalgebra.inclusion h) = f i

@[simp]

theorem NonUnitalSubalgebra.iSupLift_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x x_1 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x ∈ K i }) (hx : ↑x ∈ T) : ↑(NonUnitalSubalgebra.iSupLift K dir f hf T hT) { val := ↑x, property := hx } = ↑(f i) x

theorem NonUnitalSubalgebra.iSupLift_of_mem {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalNonAssocSemiring B] [Module R B] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x x_1 => x ≤ x_1) K} {f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x // x ∈ T }) (hx : ↑x ∈ K i) : ↑(NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = ↑(f i) { val := ↑x, property := hx }

theorem Set.smul_mem_center {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (r : R) {a : A} (ha : a ∈ Set.center A) : r • a ∈ Set.center A

def NonUnitalSubalgebra.center (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra R A

The center of a non-unital algebra is the set of elements which commute with every element. They form a non-unital subalgebra.

theorem NonUnitalSubalgebra.coe_center (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑(NonUnitalSubalgebra.center R A) = Set.center A

@[simp]

theorem NonUnitalSubalgebra.center_toNonUnitalSubsemiring (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (NonUnitalSubalgebra.center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A

@[simp]

theorem NonUnitalSubalgebra.center_toNonUnitalSubring (R : Type u_3) (A : Type u_4) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.toNonUnitalSubring (NonUnitalSubalgebra.center R A) = NonUnitalSubring.center A

@[simp]

theorem NonUnitalSubalgebra.center_eq_top (R : Type u_1) [CommSemiring R] (A : Type u_3) [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.center R A = ⊤

instance NonUnitalSubalgebra.center.instNonUnitalCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommSemiring { x // x ∈ NonUnitalSubalgebra.center R A }

instance NonUnitalSubalgebra.center.instNonUnitalCommRing {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing { x // x ∈ NonUnitalSubalgebra.center R A }

theorem NonUnitalSubalgebra.mem_center_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ NonUnitalSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b

@[simp]

theorem Set.smul_mem_centralizer {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (r : R) {a : A} (ha : a ∈ Set.centralizer s) : r • a ∈ Set.centralizer s

def NonUnitalSubalgebra.centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalSubalgebra R A

The centralizer of a set as a non-unital subalgebra.

@[simp]

theorem NonUnitalSubalgebra.coe_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : ↑(NonUnitalSubalgebra.centralizer R s) = Set.centralizer s

theorem NonUnitalSubalgebra.mem_centralizer_iff (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {z : A} : z ∈ NonUnitalSubalgebra.centralizer R s ↔ ∀ (g : A), g ∈ s → g * z = z * g

theorem NonUnitalSubalgebra.centralizer_le (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) (t : Set A) (h : s ⊆ t) : NonUnitalSubalgebra.centralizer R t ≤ NonUnitalSubalgebra.centralizer R s

@[simp]

theorem NonUnitalSubalgebra.centralizer_univ (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra.centralizer R Set.univ = NonUnitalSubalgebra.center R A

def nonUnitalSubalgebraOfNonUnitalSubsemiring {R : Type u_1} [NonUnitalSemiring R] (S : NonUnitalSubsemiring R) : NonUnitalSubalgebra ℕ R

A non-unital subsemiring is a non-unital ℕ-subalgebra.

@[simp]

theorem mem_nonUnitalSubalgebraOfNonUnitalSubsemiring {R : Type u_1} [NonUnitalSemiring R] {x : R} {S : NonUnitalSubsemiring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S

def nonUnitalSubalgebraOfNonUnitalSubring {R : Type u_1} [NonUnitalRing R] (S : NonUnitalSubring R) : NonUnitalSubalgebra ℤ R

A non-unital subring is a non-unitalsubalgebra.

@[simp]

theorem mem_nonUnitalSubalgebraOfNonUnitalSubring {R : Type u_1} [NonUnitalRing R] {x : R} {S : NonUnitalSubring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S