ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S₁ S₂ : NonUnitalStarSubalgebra R A<GOAL>S₁.toNonUnitalSubalgebra ≤ S₂.toNonUnitalSubalgebra ↔ S₁ ≤ S₂
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toNonUnitalSubring ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>↑S.toNonUnitalSubring = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<GOAL>Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubring
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S U : NonUnitalStarSubalgebra R A<GOAL>S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>↑0 = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x : ↥S<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>Semiring R'<VAR>SMul R' R<VAR>Module R' A<VAR>IsScalarTower R' R A<VAR>r : R'<VAR>x : ↥S<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x : ↥S<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>NonUnitalSubalgebraClass.subtype S = NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebraClass.subtype S)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>NonUnitalSubringClass.subtype S = ↑(NonUnitalStarSubalgebraClass.subtype S)
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S₁ S₂ : NonUnitalStarSubalgebra R A<VAR>f : F<GOAL>S₁ ≤ S₂ → NonUnitalStarSubalgebra.map f S₁ ≤ NonUnitalStarSubalgebra.map f S₂
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (NonUnitalStarSubalgebra.map f)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>NonUnitalStarSubalgebra.map (NonUnitalStarAlgHom.id R A) S = S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R C<VAR>Star C<VAR>S : NonUnitalStarSubalgebra R A<VAR>g : B →⋆ₙₐ[R] C<VAR>f : A →⋆ₙₐ[R] B<GOAL>NonUnitalStarSubalgebra.map g (NonUnitalStarSubalgebra.map f S) = NonUnitalStarSubalgebra.map (g.comp f) S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>f : F<VAR>y : B<GOAL>y ∈ NonUnitalStarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>f : F<GOAL>(NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>f : F<GOAL>↑(NonUnitalStarSubalgebra.map f S) = ⇑f '' ↑S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>f : F<VAR>U : NonUnitalStarSubalgebra R B<GOAL>NonUnitalStarSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalStarSubalgebra.comap f U
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R B<VAR>f : F<VAR>x : A<GOAL>x ∈ NonUnitalStarSubalgebra.comap f S ↔ f x ∈ S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R B<VAR>f : F<GOAL>↑(NonUnitalStarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>s : NonUnitalSubalgebra R A<VAR>h_star : ∀ x ∈ s, star x ∈ s<VAR>x : A<GOAL>x ∈ s.toNonUnitalStarSubalgebra h_star ↔ x ∈ s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>s : NonUnitalSubalgebra R A<VAR>h_star : ∀ x ∈ s, star x ∈ s<GOAL>↑(s.toNonUnitalStarSubalgebra h_star) = ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>s : NonUnitalSubalgebra R A<VAR>h_star : ∀ x ∈ s, star x ∈ s<GOAL>(s.toNonUnitalStarSubalgebra h_star).toNonUnitalSubalgebra = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>S.toNonUnitalStarSubalgebra ⋯ = S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>φ : F<VAR>y : B<GOAL>y ∈ NonUnitalStarAlgHom.range φ ↔ ∃ x, φ x = y
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>φ : F<VAR>x : A<GOAL>φ x ∈ NonUnitalStarAlgHom.range φ
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>φ : F<GOAL>↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : B →⋆ₙₐ[R] C<GOAL>NonUnitalStarAlgHom.range (g.comp f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : B →⋆ₙₐ[R] C<GOAL>NonUnitalStarAlgHom.range (g.comp f) ≤ NonUnitalStarAlgHom.range g
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalStarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>(NonUnitalStarSubalgebraClass.subtype S).comp (NonUnitalStarAlgHom.codRestrict f S hf) = ↑f
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalStarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<VAR>x : A<GOAL>↑((NonUnitalStarAlgHom.codRestrict f S hf) x) = f x
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalStarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>Function.Injective ⇑(NonUnitalStarAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>φ ψ : F<VAR>x : A<GOAL>x ∈ NonUnitalStarAlgHom.equalizer φ ψ ↔ φ x = ψ x
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>g : B → A<VAR>f : F<VAR>h : Function.LeftInverse g ⇑f<VAR>x : A<GOAL>↑((StarAlgEquiv.ofLeftInverse' h) x) = f x
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>g : B → A<VAR>f : F<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥(NonUnitalStarAlgHom.range f)<GOAL>(StarAlgEquiv.ofLeftInverse' h).symm x = g ↑x
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>Star A<VAR>NonUnitalSemiring B<VAR>Module R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>x : A<GOAL>↑((StarAlgEquiv.ofInjective' f hf) x) = f x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ star S ↔ star x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : A<GOAL>star x ∈ star S ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑(star S) = star ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>Monotone star
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑S.starClosure = ⋂ s, ⋂ (_ : ↑(NonUnitalSubsemiring.closure (↑S ∪ star ↑S)) ⊆ ↑s), ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S₁ : NonUnitalSubalgebra R A<VAR>S₂ : NonUnitalStarSubalgebra R A<VAR>h : S₁ ≤ S₂.toNonUnitalSubalgebra<GOAL>S₁.starClosure ≤ S₂
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S₁ : NonUnitalSubalgebra R A<VAR>S₂ : NonUnitalStarSubalgebra R A<GOAL>S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.starClosure.toNonUnitalSubalgebra = S ⊔ star S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>Monotone NonUnitalSubalgebra.starClosure
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>NonUnitalStarAlgebra.adjoin R s = (NonUnitalAlgebra.adjoin R s).starClosure
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>(NonUnitalStarAlgebra.adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>star s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ NonUnitalStarAlgebra.adjoin R {x}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>x : A<GOAL>star x ∈ NonUnitalStarAlgebra.adjoin R {x}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<VAR>p : (x : A) → x ∈ NonUnitalStarAlgebra.adjoin R s → Prop<VAR>a : A<VAR>ha : a ∈ NonUnitalStarAlgebra.adjoin R s<VAR>mem : ∀ (x : A) (hx : x ∈ s), p x ⋯<VAR>add : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>zero : p 0 ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯<VAR>smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (r • x) ⋯<VAR>star : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (star x) ⋯<GOAL>p a ha
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<VAR>hs : s ⊆ ↑S<GOAL>NonUnitalStarAlgebra.adjoin R s ≤ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<GOAL>NonUnitalStarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : NonUnitalStarSubalgebra R A<GOAL>NonUnitalStarAlgebra.adjoin R ↑s = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>s : Set A<GOAL>(NonUnitalStarAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>s : NonUnitalStarSubalgebra R A<GOAL>Submodule.span R ↑s = s.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.starClosure = NonUnitalStarAlgebra.adjoin R ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<GOAL>⊤.toNonUnitalSubalgebra = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>S.toNonUnitalSubalgebra = ⊤ ↔ S = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>NonUnitalSemiring B<VAR>StarRing B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>StarModule R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>NonUnitalStarSubalgebra.map f (S ⊔ T) = NonUnitalStarSubalgebra.map f S ⊔ NonUnitalStarSubalgebra.map f T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>(S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : Set (NonUnitalStarSubalgebra R A)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : Set (NonUnitalStarSubalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>S : Set (NonUnitalStarSubalgebra R A)<GOAL>(sInf S).toNonUnitalSubalgebra = sInf (NonUnitalStarSubalgebra.toNonUnitalSubalgebra '' S)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>ι : Sort u_1<VAR>S : ι → NonUnitalStarSubalgebra R A<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>StarModule R A<VAR>ι : Sort u_1<VAR>S : ι → NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i