Loogle!

Result

Found 485 declarations mentioning NonUnitalSemiring. Of these, only the first 200 are shown.

• NonUnitalSemiring 📋 Mathlib.Algebra.Ring.Defs
  (α : Type u) : Type u
• NonUnitalCommSemiring.toNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : NonUnitalCommSemiring α] : NonUnitalSemiring α
• NonUnitalRing.toNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonUnitalRing α] : NonUnitalSemiring α
• NonUnitalSemiring.toNonUnitalNonAssocSemiring 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : NonUnitalSemiring α] : NonUnitalNonAssocSemiring α
• NonUnitalSemiring.toSemigroupWithZero 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : NonUnitalSemiring α] : SemigroupWithZero α
• Semiring.toNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : Semiring α] : NonUnitalSemiring α
• IsMulCommutative.instNonUnitalCommSemiring 📋 Mathlib.Algebra.Ring.Defs
  {R : Type v} [NonUnitalSemiring R] [IsMulCommutative R] : NonUnitalCommSemiring R
• IsUnital.toSemiring 📋 Mathlib.Algebra.Ring.Defs
  {A : Type u_1} [NonUnitalSemiring A] [IsUnital A] : Semiring A
• NonUnitalCommSemiring.mk 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [toNonUnitalSemiring : NonUnitalSemiring α] (mul_comm : ∀ (a b : α), a * b = b * a) : NonUnitalCommSemiring α
• NonUnitalSemiring.mk 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring α] (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) : NonUnitalSemiring α
• NonUnitalSemiring.mul_assoc 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : NonUnitalSemiring α] (a b c : α) : a * b * c = a * (b * c)
• Nat.instNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Nat
  : NonUnitalSemiring ℕ
• Function.Injective.nonUnitalSemiring 📋 Mathlib.Algebra.Ring.InjSurj
  {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Function.Injective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) : NonUnitalSemiring S
• Function.Surjective.nonUnitalSemiring 📋 Mathlib.Algebra.Ring.InjSurj
  {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Function.Surjective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) : NonUnitalSemiring S
• Lex.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSemiring (Lex R)
• OrderDual.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSemiring Rᵒᵈ
• WithBot.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
  {α : Type u_1} [DecidableEq α] [NonUnitalSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] : NonUnitalSemiring (WithBot α)
• WithTop.instNonUnitalSemiring 📋 Mathlib.Algebra.Order.Ring.WithTop
  {α : Type u_1} [DecidableEq α] [NonUnitalSemiring α] [Subsingleton (AddUnits α)] [NoZeroDivisors α] : NonUnitalSemiring (WithTop α)
• IsUnital.toAlgebra 📋 Mathlib.Algebra.Algebra.Defs
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsUnital A] : Algebra R A
• AddOpposite.instNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSemiring Rᵃᵒᵖ
• MulOpposite.instNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSemiring Rᵐᵒᵖ
• DomAddAct.instNonUnitalSemiringOfAddOpposite 📋 Mathlib.GroupTheory.GroupAction.DomAct.Basic
  {M : Type u_1} [NonUnitalSemiring Mᵃᵒᵖ] : NonUnitalSemiring Mᵈᵃᵃ
• DomMulAct.instNonUnitalSemiringOfMulOpposite 📋 Mathlib.GroupTheory.GroupAction.DomAct.Basic
  {M : Type u_1} [NonUnitalSemiring Mᵐᵒᵖ] : NonUnitalSemiring Mᵈᵐᵃ
• Pi.nonUnitalSemiring 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type v} [(i : I) → NonUnitalSemiring (f i)] : NonUnitalSemiring ((i : I) → f i)
• LinearMap.mulLeft_mul 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] (a b : A) : LinearMap.mulLeft R (a * b) = LinearMap.mulLeft R a ∘ₗ LinearMap.mulLeft R b
• LinearMap.mulRight_mul 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) : LinearMap.mulRight R (a * b) = LinearMap.mulRight R b ∘ₗ LinearMap.mulRight R a
• ULift.nonUnitalSemiring 📋 Mathlib.Algebra.Ring.ULift
  {R : Type u} [NonUnitalSemiring R] : NonUnitalSemiring (ULift.{u_1, u} R)
• NonUnitalSubsemiringClass.toNonUnitalSemiring 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {S : Type v} (s : S) {R : Type u_1} [NonUnitalSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] : NonUnitalSemiring ↥s
• Prod.instNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S)
• NonUnitalSubsemiring.centralizer 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring R
• NonUnitalSubsemiring.centralizer_univ 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] : NonUnitalSubsemiring.centralizer Set.univ = NonUnitalSubsemiring.center R
• NonUnitalSubsemiring.centralizer_toSubsemigroup 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s : Set R) : (NonUnitalSubsemiring.centralizer s).toSubsemigroup = Subsemigroup.centralizer s
• NonUnitalSubsemiring.coe_centralizer 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s : Set R) : ↑(NonUnitalSubsemiring.centralizer s) = s.centralizer
• NonUnitalSubsemiring.decidableMemCenter 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] [DecidableEq R] [Fintype R] : DecidablePred fun x => x ∈ NonUnitalSubsemiring.center R
• NonUnitalSubsemiring.center_le_centralizer 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring.center R ≤ NonUnitalSubsemiring.centralizer s
• NonUnitalSubsemiring.centralizer_le 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s t : Set R) (h : s ⊆ t) : NonUnitalSubsemiring.centralizer t ≤ NonUnitalSubsemiring.centralizer s
• NonUnitalSubsemiring.centralizer_eq_top_iff_subset 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] {s : Set R} : NonUnitalSubsemiring.centralizer s = ⊤ ↔ s ⊆ ↑(NonUnitalSubsemiring.center R)
• NonUnitalSubsemiring.closure_le_centralizer_centralizer 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.centralizer ↑(NonUnitalSubsemiring.centralizer s)
• NonUnitalSubsemiring.mem_center_iff 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] {z : R} : z ∈ NonUnitalSubsemiring.center R ↔ ∀ (g : R), g * z = z * g
• NonUnitalSubsemiring.mem_centralizer_iff 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] {s : Set R} {z : R} : z ∈ NonUnitalSubsemiring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
• NonUnitalSubsemiring.closureNonUnitalCommSemiringOfComm 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : NonUnitalCommSemiring ↥(NonUnitalSubsemiring.closure s)
• NonUnitalSubsemiring.isMulCommutative_closure 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u_1} [NonUnitalSemiring R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : IsMulCommutative ↥(NonUnitalSubsemiring.closure s)
• NonUnitalSubsemiring.instIsMulCommutative_closure 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {S : Type u_1} {R : Type u_2} [NonUnitalSemiring R] [SetLike S R] [MulMemClass S R] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(NonUnitalSubsemiring.closure ↑s)
• List.dvd_sum 📋 Mathlib.Algebra.BigOperators.Ring.List
  {R : Type u_5} [NonUnitalSemiring R] {a : R} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum
• Multiset.dvd_sum 📋 Mathlib.Algebra.BigOperators.Ring.Multiset
  {R : Type u_4} [NonUnitalSemiring R] {s : Multiset R} {a : R} : (∀ x ∈ s, a ∣ x) → a ∣ s.sum
• Finset.dvd_sum 📋 Mathlib.Algebra.BigOperators.Ring.Finset
  {ι : Type u_1} {R : Type u_4} {s : Finset ι} [NonUnitalSemiring R] {f : ι → R} {a : R} (h : ∀ i ∈ s, a ∣ f i) : a ∣ ∑ i ∈ s, f i
• RingCon.instNonUnitalSemiringQuotient 📋 Mathlib.RingTheory.Congruence.Defs
  {R : Type u_1} [NonUnitalSemiring R] (c : RingCon R) : NonUnitalSemiring c.Quotient
• IsIdempotentElem.commute_of_anticommute 📋 Mathlib.Algebra.Ring.Idempotent
  {R : Type u_1} {a b : R} [NonUnitalSemiring R] [IsAddTorsionFree R] (ha : IsIdempotentElem a) (hab : a * b + b * a = 0) : Commute a b
• IsIdempotentElem.mul_eq_zero_of_anticommute 📋 Mathlib.Algebra.Ring.Idempotent
  {R : Type u_1} {a b : R} [NonUnitalSemiring R] [IsAddTorsionFree R] (ha : IsIdempotentElem a) (hab : a * b + b * a = 0) : a * b = 0
• AddMonoidAlgebra.nonUnitalSemiring 📋 Mathlib.Algebra.MonoidAlgebra.Defs
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddSemigroup M] : NonUnitalSemiring (AddMonoidAlgebra R M)
• MonoidAlgebra.nonUnitalSemiring 📋 Mathlib.Algebra.MonoidAlgebra.Defs
  {R : Type u_1} {M : Type u_4} [Semiring R] [Semigroup M] : NonUnitalSemiring (MonoidAlgebra R M)
• NonUnitalAlgHomClass.instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  {F : Type u_3} {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} {x✝ : Semiring R} {x✝¹ : Semiring S} {φ : R →+* S} {x✝² : NonUnitalSemiring A} {x✝³ : NonUnitalSemiring B} [Module R A] [Module S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F (↑φ) A B] : SemilinearMapClass F φ A B
• LinearMap.commute_mulLeft_right 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a b : A) : Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R b)
• NonUnitalAlgHom.lmul 📋 Mathlib.Algebra.Algebra.Bilinear
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : A →ₙₐ[R] Module.End R A
• NonUnitalAlgHom.coe_lmul_eq_mul 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : ⇑(NonUnitalAlgHom.lmul R A) = ⇑(LinearMap.mul R A)
• LinearMap.map_mul_iff 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [NonUnitalSemiring B] [Module R B] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [SMulCommClass R B B] [IsScalarTower R B B] (f : A →ₗ[R] B) : (∀ (x y : A), f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f
• AddSubmonoid.semigroup 📋 Mathlib.Algebra.Ring.Submonoid.Pointwise
  {R : Type u_2} [NonUnitalSemiring R] : Semigroup (AddSubmonoid R)
• SetSemiring.instNonUnitalSemiringOfSemigroup 📋 Mathlib.Data.Set.Semiring
  {α : Type u_1} [Semigroup α] : NonUnitalSemiring (SetSemiring α)
• Submodule.instNonUnitalSemiring 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] : NonUnitalSemiring (Submodule R A)
• Matrix.nonUnitalSemiring 📋 Mathlib.Data.Matrix.Mul
  {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] : NonUnitalSemiring (Matrix n n α)
• Matrix.isLeftRegular_iff_mulVec_injective 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {α : Type v} [NonUnitalSemiring α] [Fintype m] {A : Matrix m m α} : IsLeftRegular A ↔ Function.Injective A.mulVec
• Matrix.isRightRegular_iff_vecMul_injective 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {α : Type v} [NonUnitalSemiring α] [Fintype m] {A : Matrix m m α} : IsRightRegular A ↔ Function.Injective fun v => Matrix.vecMul v A
• Matrix.dotProduct_mulVec 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A.mulVec w = Matrix.vecMul v A ⬝ᵥ w
• Matrix.mul_right_injective_iff_mulVec_injective 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Nonempty n] {A : Matrix l m α} : (Function.Injective fun B => A * B) ↔ Function.Injective A.mulVec
• Matrix.mul_left_injective_iff_vecMul_injective 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Nonempty l] [Fintype m] {A : Matrix m n α} : (Function.Injective fun B => B * A) ↔ Function.Injective fun v => Matrix.vecMul v A
• Matrix.vecMul_vecMulVec 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (u v : m → α) (w : n → α) : Matrix.vecMul u (Matrix.vecMulVec v w) = (u ⬝ᵥ v) • w
• Matrix.mulVec_mulVec 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) : M.mulVec (N.mulVec v) = (M * N).mulVec v
• Matrix.vecMul_vecMul 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) : Matrix.vecMul (Matrix.vecMul v M) N = Matrix.vecMul v (M * N)
• Matrix.mul_vecMulVec 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (M : Matrix l m α) (x : m → α) (y : n → α) : M * Matrix.vecMulVec x y = Matrix.vecMulVec (M.mulVec x) y
• Matrix.vecMulVec_mul 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (x : l → α) (y : m → α) (M : Matrix m n α) : Matrix.vecMulVec x y * M = Matrix.vecMulVec x (Matrix.vecMul y M)
• dotProduct_assoc 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) : (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
• Matrix.dot_mulVec_eq_sum_sum 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A.mulVec w = ∑ j, ∑ i, v i * A i j * w j
• Matrix.vecMulVec_mulVec 📋 Mathlib.Data.Matrix.Mul
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (u : m → α) (v w : n → α) : (Matrix.vecMulVec u v).mulVec w = MulOpposite.op (v ⬝ᵥ w) • u
• Matrix.mul_mul_apply 📋 Mathlib.Data.Matrix.Mul
  {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (A B C : Matrix n n α) (i j : n) : (A * B * C) i j = A i ⬝ᵥ B.mulVec (C.transpose j)
• Matrix.vecMulVec_mul_vecMulVec 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (u : l → α) (v w : m → α) (x : n → α) : Matrix.vecMulVec u v * Matrix.vecMulVec w x = Matrix.vecMulVec u ((v ⬝ᵥ w) • x)
• Matrix.mul_assoc 📋 Mathlib.Data.Matrix.Mul
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) : L * M * N = L * (M * N)
• 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
• 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
• 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_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
• 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.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
• 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
• 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.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)
• 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)
• Set.smul_mem_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} (r : R) {a : A} (ha : a ∈ s.centralizer) : r • a ∈ s.centralizer
• 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.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)
• 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)
• 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
• 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.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
• MulOpposite.instStarRing 📋 Mathlib.Algebra.Star.Basic
  {R : Type u} [NonUnitalSemiring R] [StarRing R] : StarRing Rᵐᵒᵖ
• Matrix.mulVec_conjTranspose 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) : A.conjTranspose.mulVec x = star (Matrix.vecMul (star x) A)
• Matrix.star_mulVec 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) : star (M.mulVec v) = Matrix.vecMul (star v) M.conjTranspose
• Matrix.star_vecMul 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [StarRing α] (M : Matrix m n α) (v : m → α) : star (Matrix.vecMul v M) = M.conjTranspose.mulVec (star v)
• Matrix.vecMul_conjTranspose 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) : Matrix.vecMul x A.conjTranspose = star (A.mulVec (star x))
• Matrix.dotProduct_star 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v w : m → α) : v ⬝ᵥ star w = star (w ⬝ᵥ star v)
• Matrix.star_dotProduct 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v w : m → α) : star v ⬝ᵥ w = star (star w ⬝ᵥ v)
• Matrix.star_dotProduct_star 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
  {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v w : m → α) : star v ⬝ᵥ star w = star (w ⬝ᵥ v)
• Algebra.TensorProduct.instNonUnitalSemiring 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalSemiring (TensorProduct R A B)
• Algebra.TensorProduct.instNonUnitalRing 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] : NonUnitalRing (TensorProduct R A B)
• Algebra.TensorProduct.mul_assoc 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (x y z : TensorProduct R A B) : (Algebra.TensorProduct.mul ((Algebra.TensorProduct.mul x) y)) z = (Algebra.TensorProduct.mul x) ((Algebra.TensorProduct.mul y) z)
• Equiv.nonUnitalSemiring 📋 Mathlib.Algebra.Ring.TransferInstance
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalSemiring β] : NonUnitalSemiring α
• Shrink.instNonUnitalSemiring 📋 Mathlib.Algebra.Ring.Shrink
  {α : Type u_1} [Small.{v, u_1} α] [NonUnitalSemiring α] : NonUnitalSemiring (Shrink.{v, u_1} α)
• IsStarProjection.mul 📋 Mathlib.Algebra.Star.StarProjection
  {R : Type u_1} {p q : R} [NonUnitalSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : Commute p q) : IsStarProjection (p * q)
• NonUnitalStarSubalgebra.subsingleton_of_subsingleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [Subsingleton A] : Subsingleton (NonUnitalStarSubalgebra R A)
• NonUnitalStarSubalgebra.toNonUnitalSemiring 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) : NonUnitalSemiring ↥S
• NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) : S.toNonUnitalStarSubalgebra ⋯ = S
• NonUnitalSubalgebra.toNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) : NonUnitalStarSubalgebra R A
• NonUnitalSubalgebra.toNonUnitalStarSubalgebra_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) : (s.toNonUnitalStarSubalgebra h_star).toNonUnitalSubalgebra = s
• NonUnitalSubalgebra.instInvolutiveStar 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] : InvolutiveStar (NonUnitalSubalgebra R A)
• NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s) : ↑(s.toNonUnitalStarSubalgebra h_star) = ↑s
• NonUnitalStarAlgebra.span_eq_toSubmodule 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {A : Type v} [NonUnitalSemiring A] [StarRing A] {R : Type u_1} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) : Submodule.span R ↑s = s.toSubmodule
• NonUnitalStarSubalgebra.prod 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) : NonUnitalStarSubalgebra R (A × B)
• NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [Star A] {s : NonUnitalSubalgebra R A} {h_star : ∀ x ∈ s, star x ∈ s} {x : A} : x ∈ s.toNonUnitalStarSubalgebra h_star ↔ x ∈ s
• NonUnitalSubalgebra.star_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] : Monotone star
• NonUnitalSubalgebra.coe_star 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) : ↑(star S) = star ↑S
• NonUnitalStarSubalgebra.center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalStarSubalgebra R A
• NonUnitalStarSubalgebra.centralizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalStarSubalgebra R A
• NonUnitalSubalgebra.mem_star_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) (x : A) : x ∈ star S ↔ star x ∈ S
• NonUnitalSubalgebra.star_mem_star_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] (S : NonUnitalSubalgebra R A) (x : A) : star x ∈ star S ↔ x ∈ S
• NonUnitalStarSubalgebra.centralizer_univ 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalStarSubalgebra.centralizer R Set.univ = NonUnitalStarSubalgebra.center R A
• NonUnitalStarSubalgebra.center_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (NonUnitalStarSubalgebra.center R A).toNonUnitalSubalgebra = NonUnitalSubalgebra.center R A
• NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) : (S.prod S₁).toNonUnitalSubalgebra = S.prod S₁.toNonUnitalSubalgebra
• NonUnitalStarSubalgebra.coe_center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑(NonUnitalStarSubalgebra.center R A) = Set.center A
• NonUnitalStarSubalgebra.instNoZeroDivisors 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) : NoZeroDivisors ↥S
• NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : (NonUnitalStarSubalgebra.centralizer R s).toNonUnitalSubalgebra = NonUnitalSubalgebra.centralizer R (s ∪ star s)
• NonUnitalStarSubalgebra.instNonUnitalCommSemiring 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommSemiring ↥(NonUnitalStarSubalgebra.center R A)
• NonUnitalStarSubalgebra.coe_centralizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : ↑(NonUnitalStarSubalgebra.centralizer R s) = (s ∪ star s).centralizer
• NonUnitalStarSubalgebra.mem_center_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ NonUnitalStarSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b
• NonUnitalStarSubalgebra.centralizer_le 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s t : Set A) (h : s ⊆ t) : NonUnitalStarSubalgebra.centralizer R t ≤ NonUnitalStarSubalgebra.centralizer R s
• NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : CompleteLattice (NonUnitalStarSubalgebra R A)
• NonUnitalStarAlgebra.instInhabitedNonUnitalStarSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : Inhabited (NonUnitalStarSubalgebra R A)
• NonUnitalStarAlgebra.adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : NonUnitalStarSubalgebra R A
• NonUnitalSubalgebra.starClosure 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A
• NonUnitalStarSubalgebra.coe_prod 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B) : ↑(S.prod S₁) = ↑S ×ˢ ↑S₁
• NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : NonUnitalStarAlgebra.adjoin R s = (NonUnitalAlgebra.adjoin R s).starClosure
• NonUnitalStarSubalgebra.coe_centralizer_centralizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : ↑(NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)) = (s ∪ star s).centralizer.centralizer
• NonUnitalStarAlgebra.subset_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
• NonUnitalSubalgebra.starClosure_eq_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : NonUnitalSubalgebra R A) : S.starClosure = NonUnitalStarAlgebra.adjoin R ↑S
• NonUnitalSubalgebra.star_adjoin_comm 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s)
• NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : (NonUnitalStarAlgebra.adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s)
• NonUnitalStarAlgebra.star_subset_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : star s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
• NonUnitalStarSubalgebra.mem_centralizer_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {z : A} : z ∈ NonUnitalStarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
• NonUnitalStarAlgebra.self_mem_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (x : A) : x ∈ NonUnitalStarAlgebra.adjoin R {x}
• NonUnitalStarAlgebra.mem_adjoin_of_mem 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s : Set A} {x : A} (hx : x ∈ s) : x ∈ NonUnitalStarAlgebra.adjoin R s
• NonUnitalSubalgebra.starClosure_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] : Monotone NonUnitalSubalgebra.starClosure
• NonUnitalStarAlgebra.adjoin_eq 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : NonUnitalStarSubalgebra R A) : NonUnitalStarAlgebra.adjoin R ↑s = s
• NonUnitalStarAlgebra.star_self_mem_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (x : A) : star x ∈ NonUnitalStarAlgebra.adjoin R {x}
• NonUnitalStarAlgHom.subsingleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Subsingleton (NonUnitalStarSubalgebra R A)] : Subsingleton (A →⋆ₙₐ[R] B)
• NonUnitalStarAlgebra.adjoin_eq_span 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : (NonUnitalStarAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))
• NonUnitalStarAlgebra.adjoin_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s t : Set A} (H : s ⊆ t) : NonUnitalStarAlgebra.adjoin R s ≤ NonUnitalStarAlgebra.adjoin R t
• NonUnitalStarAlgebra.commute_of_mem_adjoin_self 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {a b : A} [IsStarNormal a] (hb : b ∈ NonUnitalStarAlgebra.adjoin R {a}) : Commute a b
• NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) : S.starClosure.toNonUnitalSubalgebra = S ⊔ star S
• NonUnitalStarAlgebra.commute_of_mem_adjoin_singleton_of_commute 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {a b c : A} (hc : c ∈ NonUnitalStarAlgebra.adjoin R {b}) (h : Commute a b) (h_star : Commute a (star b)) : Commute a c
• NonUnitalStarAlgebra.gc 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe
• NonUnitalStarAlgebra.gi 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : GaloisInsertion (NonUnitalStarAlgebra.adjoin R) SetLike.coe
• NonUnitalStarAlgebra.commute_of_mem_adjoin_of_forall_mem_commute 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {a b : A} {s : Set A} (hb : b ∈ NonUnitalStarAlgebra.adjoin R s) (h : ∀ b ∈ s, Commute a b) (h_star : ∀ b ∈ s, Commute a (star b)) : Commute a b
• NonUnitalStarSubalgebra.mem_prod 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {S : NonUnitalStarSubalgebra R A} {S₁ : NonUnitalStarSubalgebra R B} {x : A × B} : x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
• NonUnitalSubalgebra.coe_starClosure 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) : ↑S.starClosure = ↑(S ⊔ star S)
• NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (s : Set A) : NonUnitalStarAlgebra.adjoin R s ≤ NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)
• NonUnitalStarAlgebra.adjoin_le 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A} (hs : s ⊆ ↑S) : NonUnitalStarAlgebra.adjoin R s ≤ S
• NonUnitalStarAlgebra.adjoin_le_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A} : NonUnitalStarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
• NonUnitalSubalgebra.starClosure_le 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} (h : S₁ ≤ S₂.toNonUnitalSubalgebra) : S₁.starClosure ≤ S₂
• NonUnitalSubalgebra.starClosure_le_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A} : S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra
• NonUnitalSubalgebra.mem_starClosure 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : NonUnitalSubalgebra R A) {x : A} : x ∈ S.starClosure ↔ x ∈ S ⊔ star S
• NonUnitalStarAlgebra.adjoinNonUnitalCommSemiringOfComm 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : NonUnitalCommSemiring ↥(NonUnitalStarAlgebra.adjoin R s)
• NonUnitalStarAlgebra.coe_iInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A} : ↑(⨅ i, S i) = ⋂ i, ↑(S i)
• NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} (S : ι → NonUnitalStarSubalgebra R A) : (⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra
• NonUnitalStarAlgebra.isMulCommutative_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] (S : NonUnitalStarSubalgebra R A) [IsMulCommutative ↥S] : IsMulCommutative ↥S.toNonUnitalSubalgebra
• NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)) : (sInf S).toNonUnitalSubalgebra = sInf (NonUnitalStarSubalgebra.toNonUnitalSubalgebra '' S)
• NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S T : NonUnitalStarSubalgebra R A) : (S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra
• NonUnitalStarAlgebra.mem_iInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A} {x : A} : x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
• NonUnitalStarSubalgebra.prod_mono 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B} : S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
• NonUnitalStarAlgebra.mem_sup_left 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ S → x ∈ S ⊔ T
• NonUnitalStarAlgebra.mem_sup_right 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ T → x ∈ S ⊔ T
• NonUnitalStarAlgebra.coe_inf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S T : NonUnitalStarSubalgebra R A) : ↑(S ⊓ T) = ↑S ∩ ↑T
• NonUnitalStarSubalgebra.comap_center_le_center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {F : Type u_1} [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Injective ⇑f) : NonUnitalStarSubalgebra.comap f (NonUnitalStarSubalgebra.center R B) ≤ NonUnitalStarSubalgebra.center R A
• NonUnitalStarSubalgebra.map_center_le_center 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {F : Type u_1} [IsScalarTower R B B] [SMulCommClass R B B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] {f : F} (hf : Function.Surjective ⇑f) : NonUnitalStarSubalgebra.map f (NonUnitalStarSubalgebra.center R A) ≤ NonUnitalStarSubalgebra.center R B
• NonUnitalStarSubalgebra.map_center_eq 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {F : Type u_1} [IsScalarTower R B B] [SMulCommClass R B B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] (f : F) : NonUnitalStarSubalgebra.map f (NonUnitalStarSubalgebra.center R A) = NonUnitalStarSubalgebra.center R B
• NonUnitalStarAlgebra.mem_sInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : Set (NonUnitalStarSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
• NonUnitalStarAlgebra.mem_inf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
• NonUnitalStarAlgebra.mul_mem_sup 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T
• NonUnitalStarAlgebra.coe_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : ↑⊤ = Set.univ
• NonUnitalStarSubalgebra.coe_iSup_of_directed 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] {ι : Type u_1} [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A} (dir : Directed (fun x1 x2 => x1 ≤ x2) S) : ↑(iSup S) = ⋃ i, ↑(S i)
• NonUnitalStarAlgebra.coe_bot 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : ↑⊥ = {0}
• NonUnitalStarSubalgebra.center_prod 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] : NonUnitalStarSubalgebra.center R (A × B) = (NonUnitalStarSubalgebra.center R A).prod (NonUnitalStarSubalgebra.center R B)
• NonUnitalStarAlgebra.isMulCommutative_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (a : A) [IsStarNormal a] : IsMulCommutative ↥(NonUnitalStarAlgebra.adjoin R {a})
• NonUnitalStarAlgebra.mem_top 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {x : A} : x ∈ ⊤
• NonUnitalStarAlgebra.coe_sInf 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)) : ↑(sInf S) = ⋂ s ∈ S, ↑s
• NonUnitalStarAlgebra.mem_bot 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {x : A} : x ∈ ⊥ ↔ x = 0
• NonUnitalStarAlgHom.map_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (s : Set A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)
• NonUnitalStarAlgebra.instIsMulCommutative_adjoin 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : Type u_1} [SetLike S A] [MulMemClass S A] [StarMemClass S A] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(NonUnitalStarAlgebra.adjoin R ↑s)
• NonUnitalStarAlgHom.map_adjoin_singleton 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalSemiring A] [StarRing A] [Module R A] [NonUnitalSemiring B] [StarRing B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] [StarRing R] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) (x : A) : NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R {x}) = NonUnitalStarAlgebra.adjoin R {f x}
• NonUnitalStarAlgebra.eq_top_iff 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {S : NonUnitalStarSubalgebra R A} : S = ⊤ ↔ ∀ (x : A), x ∈ S

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