Loogle!

Result

Found 283 declarations mentioning NonUnitalSubalgebra. Of these, only the first 200 are shown.

• NonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Type v
• nonUnitalSubalgebraOfNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) : NonUnitalSubalgebra ℕ R
• nonUnitalSubalgebraOfNonUnitalSubring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} [NonUnitalNonAssocRing R] (S : NonUnitalSubring R) : NonUnitalSubalgebra ℤ R
• NonUnitalSubalgebra.instPartialOrder 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : PartialOrder (NonUnitalSubalgebra R A)
• NonUnitalSubalgebra.instSetLike 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SetLike (NonUnitalSubalgebra R A) A
• NonUnitalSubalgebra.subsingleton_of_subsingleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Subsingleton A] : Subsingleton (NonUnitalSubalgebra R A)
• NonUnitalSubalgebra.toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) : NonUnitalSubsemiring A
• NonUnitalSubalgebra.instNonUnitalSubsemiringClass 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A
• NonUnitalSubalgebra.toNonUnitalSubsemiring_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring
• NonUnitalSubalgebra.toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) : Submodule R A
• NonUnitalSubalgebra.toNonUnitalSubring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubring A
• NonUnitalSubalgebra.toSubmodule_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective NonUnitalSubalgebra.toSubmodule
• NonUnitalSubalgebra.toNonUnitalSubring_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : Function.Injective NonUnitalSubalgebra.toNonUnitalSubring
• NonUnitalSubalgebra.instNonUnitalSubringClass 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonUnitalSubringClass (NonUnitalSubalgebra R A) A
• NonUnitalSubalgebra.copy 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalSubalgebra.instInhabitedSubtypeMem 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : Inhabited ↥S
• NonUnitalSubalgebra.toNonUnitalNonAssocSemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalNonAssocSemiring ↥S
• NonUnitalSubalgebra.coe_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toNonUnitalSubsemiring = ↑S
• NonUnitalSubalgebra.toNonUnitalSubsemiring_inj 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s t : NonUnitalSubalgebra R A} : s.toNonUnitalSubsemiring = t.toNonUnitalSubsemiring ↔ s = t
• NonUnitalSubalgebra.toNonUnitalSubsemiring' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubsemiring A
• NonUnitalSubalgebra.copy_eq 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : S.copy s hs = S
• NonUnitalSubalgebra.toNonUnitalSemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSemiring ↥S
• mem_nonUnitalSubalgebraOfNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} {S : NonUnitalSubsemiring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S
• NonUnitalSubalgebra.toSubmodule_inj 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s t : NonUnitalSubalgebra R A} : s.toSubmodule = t.toSubmodule ↔ s = t
• NonUnitalAlgebra.span_eq_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (s : NonUnitalSubalgebra R A) : Submodule.span R ↑s = s.toSubmodule
• NonUnitalSubalgebra.prod 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R (A × B)
• mem_nonUnitalSubalgebraOfNonUnitalSubring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} [NonUnitalNonAssocRing R] {x : R} {S : NonUnitalSubring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S
• NonUnitalSubalgebra.coe_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toSubmodule = ↑S
• NonUnitalSubalgebra.mem_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S
• NonUnitalSubalgebra.coe_copy 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : ↑(S.copy s hs) = s
• NonUnitalSubalgebra.toNonUnitalCommSemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommSemiring ↥S
• NonUnitalSubalgebra.toNonUnitalNonAssocRing 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalNonAssocRing ↥S
• NonUnitalSubalgebra.coe_toNonUnitalSubring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toNonUnitalSubring = ↑S
• NonUnitalSubalgebra.toNonUnitalSubring_inj 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S U : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U
• NonUnitalAlgHom.range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : NonUnitalSubalgebra R B
• NonUnitalAlgHom.equalizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (ϕ ψ : F) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.toNonUnitalSubring' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubring A
• NonUnitalSubalgebra.instSMulMemClass 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SMulMemClass (NonUnitalSubalgebra R A) R A
• NonUnitalSubalgebra.comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R B
• NonUnitalSubalgebra.toNonUnitalRing 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalRing ↥S
• NonUnitalSubalgebra.ofClass 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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] [SMulMemClass S R A] (s : S) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.toSubmodule' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o Submodule R A
• NonUnitalSubalgebra.ext 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) : S = T
• NonUnitalSubalgebra.mem_carrier 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s : NonUnitalSubalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s
• NonUnitalSubalgebra.ext_iff 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} : S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T
• NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : S.toSubmodule.toNonUnitalSubalgebra ⋯ = S
• NonUnitalSubalgebra.mem_toNonUnitalSubring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ S.toNonUnitalSubring ↔ x ∈ S
• NonUnitalSubalgebra.mem_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) {x : A} : x ∈ S.toSubmodule ↔ x ∈ S
• NonUnitalSubalgebra.toNonUnitalCommRing 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [NonUnitalCommRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommRing ↥S
• NonUnitalSubalgebra.instModule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : Module R ↥S
• NonUnitalSubalgebra.map_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (NonUnitalSubalgebra.map f)
• NonUnitalAlgHom.coe_range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ
• NonUnitalSubalgebra.instIsTorsionFree 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Module.IsTorsionFree R A] : Module.IsTorsionFree R ↥S
• NonUnitalAlgHom.fintypeRange 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [Fintype A] [DecidableEq B] (φ : F) : Fintype ↥(NonUnitalAlgHom.range φ)
• NonUnitalAlgHom.mem_range_self 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (x : A) : φ x ∈ NonUnitalAlgHom.range φ
• NonUnitalSubalgebra.ofClass_carrier 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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] [SMulMemClass S R A] (s : S) : ↑(NonUnitalSubalgebra.ofClass s) = ↑s
• NonUnitalAlgHom.mem_range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) {y : B} : y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, φ x = y
• NonUnitalAlgHom.mem_equalizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ ψ : F) (x : A) : x ∈ NonUnitalAlgHom.equalizer φ ψ ↔ φ x = ψ x
• NonUnitalSubalgebra.coe_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) : ↑(NonUnitalSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
• NonUnitalSubalgebra.coe_map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F) : ↑(NonUnitalSubalgebra.map f S) = ⇑f '' ↑S
• NonUnitalSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)
• NonUnitalSubalgebra.prod_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule
• NonUnitalSubalgebra.mem_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A) : x ∈ NonUnitalSubalgebra.comap f S ↔ f x ∈ S
• NonUnitalSubalgebra.mk 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (toNonUnitalSubsemiring : NonUnitalSubsemiring A) (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.mem_map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B} : y ∈ NonUnitalSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
• NonUnitalSubalgebra.coe_prod 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : ↑(S.prod S₁) = ↑S ×ˢ ↑S₁
• Submodule.toNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalSubalgebra.smul_mem' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) (c : R) {x : A} : x ∈ self.carrier → c • x ∈ self.carrier
• NonUnitalSubalgebra.map_mono 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S₁ S₂ : NonUnitalSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.map f S₂
• NonUnitalSubalgebra.map_le 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A 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
• NonUnitalSubalgebra.map_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule
• NonUnitalSubalgebra.coe_zero 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : ↑0 = 0
• NonUnitalSubalgebra.map_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
• NonUnitalSubalgebra.center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra R A
• NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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)
• NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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)
• NonUnitalAlgebra.adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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
• Submodule.coe_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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) : ↑(p.toNonUnitalSubalgebra h_mul) = ↑p
• NonUnitalSubalgebra.mem_prod 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
• NonUnitalSubalgebra.instModule' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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' ↥S
• NonUnitalSubalgebra.map_id 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalSubalgebra.toSubmoduleEquiv 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↥S.toSubmodule ≃ₗ[R] ↥S
• NonUnitalAlgebra.subset_adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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)
• NonUnitalSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : CanLift (Set A) (NonUnitalSubalgebra R A) SetLike.coe fun s => 0 ∈ s ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R) {x : A}, x ∈ s → r • x ∈ s
• NonUnitalSubalgebra.coe_center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑(NonUnitalSubalgebra.center R A) = Set.center A
• NonUnitalSubalgebra.center.instNonUnitalCommSemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommSemiring ↥(NonUnitalSubalgebra.center R A)
• NonUnitalAlgebra.adjoin_eq 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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) : NonUnitalAlgebra.adjoin R ↑s = s
• Submodule.mem_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p
• NonUnitalAlgebra.self_mem_adjoin_singleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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}
• NonUnitalSubalgebra.centralizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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
• NonUnitalAlgebra.mem_adjoin_of_mem 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {x : A} (hx : x ∈ s) : x ∈ NonUnitalAlgebra.adjoin R s
• NonUnitalAlgebra.adjoin_mono 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s t : Set A} (H : s ⊆ t) : NonUnitalAlgebra.adjoin R s ≤ NonUnitalAlgebra.adjoin R t
• NonUnitalSubalgebra.noZeroDivisors 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] (S : NonUnitalSubalgebra R A) : NoZeroDivisors ↥S
• NonUnitalSubalgebra.centralizer_univ 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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
• NonUnitalSubalgebra.coe_eq_zero 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : ↥S} : ↑x = 0 ↔ x = 0
• NonUnitalSubalgebra.prod_mono 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} : S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
• NonUnitalAlgebra.gc 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.gi 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.adjoin_le 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.adjoin_le_iff 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgHom.subsingleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [Subsingleton (NonUnitalSubalgebra R A)] : Subsingleton (A →ₙₐ[R] B)
• NonUnitalSubalgebra.coe_centralizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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) = s.centralizer
• NonUnitalAlgHom.codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : A →ₙₐ[R] ↥S
• Submodule.toNonUnitalSubalgebra_mk 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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) : p.toNonUnitalSubalgebra hmul = { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }
• NonUnitalAlgebra.sInf_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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)
• NonUnitalAlgebra.adjoin_union 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s t : Set A) : NonUnitalAlgebra.adjoin R (s ∪ t) = NonUnitalAlgebra.adjoin R s ⊔ NonUnitalAlgebra.adjoin R t
• NonUnitalAlgebra.inf_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : (S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring
• NonUnitalAlgebra.commute_of_mem_adjoin_self 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b : A} (hb : b ∈ NonUnitalAlgebra.adjoin R {a}) : Commute a b
• NonUnitalSubalgebra.center.instNonUnitalCommRing 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing ↥(NonUnitalSubalgebra.center R A)
• NonUnitalAlgebra.coe_iInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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)
• NonUnitalSubalgebra.centralizer_le 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s t : Set A) (h : s ⊆ t) : NonUnitalSubalgebra.centralizer R t ≤ NonUnitalSubalgebra.centralizer R s
• NonUnitalAlgHom.rangeRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] ↥(NonUnitalAlgHom.range f)
• NonUnitalAlgebra.commute_of_mem_adjoin_singleton_of_commute 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b c : A} (hc : c ∈ NonUnitalAlgebra.adjoin R {b}) (h : Commute a b) : Commute a c
• NonUnitalAlgebra.iInf_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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).toSubmodule = ⨅ i, (S i).toSubmodule
• NonUnitalSubalgebra.mem_center_iff 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b : A} {s : Set A} (hb : b ∈ NonUnitalAlgebra.adjoin R s) (h : ∀ b ∈ s, Commute a b) : Commute a b
• NonUnitalAlgebra.mem_sup_left 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ S → x ∈ S ⊔ T
• NonUnitalAlgebra.mem_sup_right 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ T → x ∈ S ⊔ T
• NonUnitalAlgebra.mem_iInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.coe_inf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : ↑(S ⊓ T) = ↑S ∩ ↑T
• NonUnitalAlgebra.inf_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : (S ⊓ T).toSubmodule = S.toSubmodule ⊓ T.toSubmodule
• NonUnitalAlgebra.adjoin_le_centralizer_centralizer 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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) : NonUnitalAlgebra.adjoin R s ≤ NonUnitalSubalgebra.centralizer R ↑(NonUnitalSubalgebra.centralizer R s)
• NonUnitalAlgebra.sInf_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S)
• NonUnitalSubalgebra.mem_centralizer_iff 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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 ∈ s, g * z = z * g
• NonUnitalAlgebra.adjoinNonUnitalCommSemiringOfComm 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : NonUnitalCommSemiring ↥(NonUnitalAlgebra.adjoin R s)
• NonUnitalSubalgebra.inclusion 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : ↥S →ₙₐ[R] ↥T
• NonUnitalAlgebra.mem_sInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ∈ S, x ∈ p
• NonUnitalAlgebra.mem_inf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
• NonUnitalSubalgebra.coe_smul 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [SMul R' R] [SMul R' A] [IsScalarTower R' R A] (r : R') (x : ↥S) : ↑(r • x) = r • ↑x
• NonUnitalAlgebra.adjoin_univ 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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 = ⊤
• NonUnitalAlgebra.top_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubsemiring = ⊤
• NonUnitalAlgebra.coe_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊤ = Set.univ
• NonUnitalAlgebra.adjoin_empty 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalAlgebra.adjoin R ∅ = ⊥
• NonUnitalAlgebra.mul_mem_sup 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T
• NonUnitalSubalgebra.coe_iSup_of_directed 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {S : ι → NonUnitalSubalgebra R A} (dir : Directed (fun x1 x2 => x1 ≤ x2) S) : ↑(iSup S) = ⋃ i, ↑(S i)
• NonUnitalAlgebra.coe_sInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ∈ S, ↑s
• NonUnitalAlgebra.mem_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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.coe_bot 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊥ = {0}
• NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 = ⊤
• NonUnitalAlgebra.mem_bot 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalAlgebra.toSubmodule_bot 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊥.toSubmodule = ⊥
• NonUnitalAlgebra.top_toSubmodule 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toSubmodule = ⊤
• NonUnitalAlgebra.eq_top_iff 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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
• NonUnitalSubalgebra.coe_add 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x y : ↥S) : ↑(x + y) = ↑x + ↑y
• NonUnitalSubalgebra.coe_mul 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x y : ↥S) : ↑(x * y) = ↑x * ↑y
• NonUnitalAlgebra.toSubmodule_eq_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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.toSubmodule = ⊤ ↔ S = ⊤
• NonUnitalAlgebra.isMulCommutative_adjoin_singleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : A) : IsMulCommutative ↥(NonUnitalAlgebra.adjoin R {x})
• NonUnitalAlgebra.adjoinNonUnitalCommRingOfComm 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (R : Type u_3) {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : NonUnitalCommRing ↥(NonUnitalAlgebra.adjoin R s)
• NonUnitalAlgebra.isMulCommutative_adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : IsMulCommutative ↥(NonUnitalAlgebra.adjoin R s)
• NonUnitalSubalgebra.inclusion_self 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : NonUnitalSubalgebra.inclusion ⋯ = NonUnitalAlgHom.id R ↥S
• NonUnitalAlgebra.instIsMulCommutative_adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : Type u_3} [SetLike S A] [MulMemClass S A] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(NonUnitalAlgebra.adjoin R ↑s)
• NonUnitalAlgHom.map_adjoin 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (s : Set A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (⇑f '' s)
• NonUnitalAlgebra.toNonUnitalSubring_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_2} {A : Type u_3} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubring = ⊤
• NonUnitalAlgHom.map_adjoin_singleton 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (x : A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R {x}) = NonUnitalAlgebra.adjoin R {f x}
• NonUnitalSubalgebra.center_eq_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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 = ⊤
• NonUnitalSubalgebra.map_center_eq 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [EquivLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : NonUnitalSubalgebra.map f (NonUnitalSubalgebra.center R A) = NonUnitalSubalgebra.center R B
• NonUnitalAlgebra.range_id 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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) = ⊤
• NonUnitalAlgHom.coe_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A 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
• NonUnitalAlgHom.injective_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A 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
• NonUnitalSubalgebra.map_center_le_center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Surjective ⇑f) : NonUnitalSubalgebra.map f (NonUnitalSubalgebra.center R A) ≤ NonUnitalSubalgebra.center R B
• NonUnitalSubalgebra.coe_neg 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x : ↥S) : ↑(-x) = -↑x
• NonUnitalSubalgebra.comap_center_le_center 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {F : Type u_4} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) : NonUnitalSubalgebra.comap f (NonUnitalSubalgebra.center R B) ≤ NonUnitalSubalgebra.center R A
• NonUnitalAlgHom.subtype_comp_codRestrict 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : (NonUnitalSubalgebraClass.subtype S).comp (NonUnitalAlgHom.codRestrict f S hf) = NonUnitalAlgHomClass.toNonUnitalAlgHom f
• NonUnitalAlgebra.map_iInf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)
• NonUnitalAlgebra.map_sup 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T
• NonUnitalAlgebra.map_inf 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊓ T) = NonUnitalSubalgebra.map f S ⊓ NonUnitalSubalgebra.map f T
• NonUnitalAlgebra.toNonUnitalSubring_eq_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = ⊤ ↔ S = ⊤
• NonUnitalAlgHom.range_comp_le_range 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 (g.comp f) ≤ NonUnitalAlgHom.range g
• NonUnitalSubalgebra.isMulCommutative_iSup 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} [Nonempty ι] {S : ι → NonUnitalSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] (dir : Directed (fun x1 x2 => x1 ≤ x2) S) : IsMulCommutative ↥(⨆ i, S i)
• NonUnitalAlgebra.range_eq_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  (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
• NonUnitalSubalgebra.center_prod 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] : NonUnitalSubalgebra.center R (A × B) = (NonUnitalSubalgebra.center R A).prod (NonUnitalSubalgebra.center R B)
• NonUnitalSubalgebra.instSMulCommClass 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [SMulCommClass R A A] : SMulCommClass R ↥S ↥S
• NonUnitalAlgebra.map_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊤ = NonUnitalAlgHom.range f
• NonUnitalSubalgebra.inclusion_injective 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : Function.Injective ⇑(NonUnitalSubalgebra.inclusion h)
• NonUnitalSubalgebra.coe_inclusion 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : ↥S) : ↑((NonUnitalSubalgebra.inclusion h) s) = ↑s
• NonUnitalAlgHom.range_comp 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 (g.comp f) = NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f)
• NonUnitalSubalgebra.range_val 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S
• NonUnitalSubalgebra.map_map 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [NonUnitalNonAssocSemiring C] [Module R A] [Module R B] [Module R C] (S : NonUnitalSubalgebra R A) (g : B →ₙₐ[R] C) (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map g (NonUnitalSubalgebra.map f S) = NonUnitalSubalgebra.map (g.comp f) S
• NonUnitalSubalgebra.inclusion_mk 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) : (NonUnitalSubalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
• NonUnitalAlgebra.comap_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.comap f ⊤ = ⊤
• NonUnitalAlgebra.map_bot 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊥ = ⊥
• NonUnitalSubalgebra.inclusion_right 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) : (NonUnitalSubalgebra.inclusion h) ⟨↑x, m⟩ = x
• NonUnitalAlgebra.adjoin_induction 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 : A) → x ∈ NonUnitalAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx → p (r • x) ⋯) {x : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s) : p x hx
• NonUnitalSubalgebra.prod_inf_prod 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
• NonUnitalSubalgebra.coe_sub 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} (x y : ↥S) : ↑(x - y) = ↑x - ↑y
• NonUnitalAlgebra.toTop 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : A →ₙₐ[R] ↥⊤
• NonUnitalSubalgebra.instIsScalarTower' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ↥S
• NonUnitalSubalgebra.instIsMulCommutative_iSup 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Type u_2} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι] {S : ι →o NonUnitalSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] : IsMulCommutative ↥(⨆ i, S i)
• NonUnitalSubalgebra.instSMulCommClass' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 ↥S
• NonUnitalSubalgebra.instIsScalarTowerSubtypeMem 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [IsScalarTower R A A] : IsScalarTower R ↥S ↥S
• NonUnitalSubalgebra.iSupLift 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (dir : Directed (fun x1 x2 => x1 ≤ x2) K) (f : (i : ι) → ↥(K i) →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)) (T : NonUnitalSubalgebra R A) (hT : T = iSup K) : ↥T →ₙₐ[R] B
• NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
• NonUnitalSubalgebra.iSupLift_comp_inclusion 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalSubalgebra.inclusion h) = f i
• NonUnitalSubalgebra.prod_top 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] : ⊤.prod ⊤ = ⊤
• NonUnitalAlgebra.adjoin_induction₂ 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {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 y : A) → x ∈ NonUnitalAlgebra.adjoin R s → y ∈ NonUnitalAlgebra.adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p 0 x ⋯ hx) (zero_right : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x 0 hx ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (smul_left : ∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x (r • y) hx ⋯) {x y : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) : p x y hx hy
• NonUnitalSubalgebra.iSupLift_of_mem 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
• NonUnitalSubalgebra.iSupLift_mk 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
• NonUnitalSubalgebra.inclusion_inclusion 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) : (NonUnitalSubalgebra.inclusion htu) ((NonUnitalSubalgebra.inclusion hst) x) = (NonUnitalSubalgebra.inclusion ⋯) x
• NonUnitalSubalgebra.iSupLift_inclusion 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalSubalgebra.inclusion h) x) = (f i) x

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c