ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>(ModuleCat.kernelIsoKer f).hom ≫ (LinearMap.ker f).subtype = CategoryTheory.Limits.kernel.ι f
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>CategoryTheory.Limits.cokernel.π f ≫ (ModuleCat.cokernelIsoRangeQuotient f).hom = (LinearMap.range f).mkQ
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>ModuleCat.asHomLeft (LinearMap.range f).mkQ ≫ (ModuleCat.cokernelIsoRangeQuotient f).inv = CategoryTheory.Limits.cokernel.π f
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x y : ↑N<VAR>m : ↑M<VAR>w : x = y + f m<GOAL>(CategoryTheory.Limits.cokernel.π f) x = (CategoryTheory.Limits.cokernel.π f) y
<VAR>A B : CommRingCat<VAR>M : ModuleCat ↑B<VAR>f : A ⟶ B<VAR>D : M.Derivation f<VAR>b b' : ↑B<GOAL>D.d (b + b') = D.d b + D.d b'
<VAR>A B : CommRingCat<VAR>M : ModuleCat ↑B<VAR>f : A ⟶ B<VAR>D : M.Derivation f<VAR>b b' : ↑B<GOAL>D.d (b * b') = b • D.d b' + b' • D.d b
<VAR>A B : CommRingCat<VAR>M : ModuleCat ↑B<VAR>f : A ⟶ B<VAR>D : M.Derivation f<VAR>a : ↑A<GOAL>D.d (f a) = 0
<VAR>A B : CommRingCat<VAR>f : A ⟶ B<VAR>M : ModuleCat ↑B<VAR>α β : CommRingCat.KaehlerDifferential f ⟶ M<VAR>h : ∀ (b : ↑B), α (CommRingCat.KaehlerDifferential.d b) = β (CommRingCat.KaehlerDifferential.d b)<GOAL>α = β
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>b : ↑B<GOAL>(CommRingCat.KaehlerDifferential.map fac) (CommRingCat.KaehlerDifferential.d b) = CommRingCat.KaehlerDifferential.d (g' b)
<VAR>A B : CommRingCat<VAR>f : A ⟶ B<VAR>M : ModuleCat ↑B<VAR>D : M.Derivation f<VAR>b : ↑B<GOAL>D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>self : StarSubalgebra R A<VAR>a : A<GOAL>a ∈ self.carrier → star a ∈ self.carrier
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : StarSubalgebra R A<VAR>x : A<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : Subalgebra R A<VAR>h : ∀ {a : A}, a ∈ S.carrier → star a ∈ S.carrier<GOAL>↑{ toSubalgebra := S, star_mem' := h } = ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toSubalgebra ↔ x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>↑S.toSubalgebra = ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<GOAL>Function.Injective StarSubalgebra.toSubalgebra
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S U : StarSubalgebra R A<GOAL>S.toSubalgebra = U.toSubalgebra ↔ S = U
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<GOAL>S₁.toSubalgebra ≤ S₂.toSubalgebra ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>(algebraMap R A).rangeS ≤ S.toSubsemiring
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>Set.range ⇑(algebraMap R A) ⊆ ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>Set.range ⇑(algebraMap R A) ≤ ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>x : A<VAR>hx : x ∈ S<VAR>r : R<GOAL>r • x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>⇑S.subtype = Subtype.val
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>x : ↥S<GOAL>S.subtype x = ↑x
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>S.val = S.subtype.toAlgHom
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<GOAL>∀ (a : ↥S₁), (StarSubalgebra.inclusion h) a = Subtype.map id h a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<GOAL>Function.Injective ⇑(StarSubalgebra.inclusion h)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<GOAL>S₂.subtype.comp (StarSubalgebra.inclusion h) = S₁.subtype
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S₁ S₂ : StarSubalgebra R A<VAR>f : A →⋆ₐ[R] B<GOAL>S₁ ≤ S₂ → StarSubalgebra.map f S₁ ≤ StarSubalgebra.map f S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (StarSubalgebra.map f)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>StarSubalgebra.map (StarAlgHom.id R A) S = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>Semiring C<VAR>StarRing C<VAR>Algebra R C<VAR>StarModule R C<VAR>S : StarSubalgebra R A<VAR>g : B →⋆ₐ[R] C<VAR>f : A →⋆ₐ[R] B<GOAL>StarSubalgebra.map g (StarSubalgebra.map f S) = StarSubalgebra.map (g.comp f) S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R A<VAR>f : A →⋆ₐ[R] B<VAR>y : B<GOAL>y ∈ StarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R A<VAR>f : A →⋆ₐ[R] B<GOAL>(StarSubalgebra.map f S).toSubalgebra = Subalgebra.map f.toAlgHom S.toSubalgebra
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R A<VAR>f : A →⋆ₐ[R] B<GOAL>↑(StarSubalgebra.map f S) = ⇑f '' ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R A<VAR>f : A →⋆ₐ[R] B<VAR>U : StarSubalgebra R B<GOAL>StarSubalgebra.map f S ≤ U ↔ S ≤ StarSubalgebra.comap f U
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<GOAL>GaloisConnection (StarSubalgebra.map f) (StarSubalgebra.comap f)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S₁ S₂ : StarSubalgebra R B<VAR>f : A →⋆ₐ[R] B<GOAL>S₁ ≤ S₂ → StarSubalgebra.comap f S₁ ≤ StarSubalgebra.comap f S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (StarSubalgebra.comap f)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>StarSubalgebra.comap (StarAlgHom.id R A) S = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>Semiring C<VAR>StarRing C<VAR>Algebra R C<VAR>StarModule R C<VAR>S : StarSubalgebra R C<VAR>g : B →⋆ₐ[R] C<VAR>f : A →⋆ₐ[R] B<GOAL>StarSubalgebra.comap f (StarSubalgebra.comap g S) = StarSubalgebra.comap (g.comp f) S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R B<VAR>f : A →⋆ₐ[R] B<VAR>x : A<GOAL>x ∈ StarSubalgebra.comap f S ↔ f x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>Semiring B<VAR>StarRing B<VAR>Algebra R B<VAR>StarModule R B<VAR>S : StarSubalgebra R B<VAR>f : A →⋆ₐ[R] B<GOAL>↑(StarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : Set A<GOAL>↑(StarSubalgebra.centralizer R s) = (s ∪ star s).centralizer
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : Set A<VAR>z : A<GOAL>z ∈ StarSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s t : Set A<VAR>h : s ⊆ t<GOAL>StarSubalgebra.centralizer R t ≤ StarSubalgebra.centralizer R s
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<VAR>x : A<GOAL>x ∈ star S ↔ star x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<VAR>x : A<GOAL>star x ∈ star S ↔ x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<GOAL>↑(star S) = star ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>Monotone star
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>star (Algebra.adjoin R s) = Algebra.adjoin R (star s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<GOAL>↑S.starClosure = ⋂ t, ⋂ (_ : Set.range ⇑(algebraMap R A) ⊆ ↑t ∧ ↑S ⊆ ↑t ∧ star ↑S ⊆ ↑t), ↑t
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<GOAL>S.starClosure.toSubalgebra = S ⊔ star S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S₁ : Subalgebra R A<VAR>S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂.toSubalgebra<GOAL>S₁.starClosure ≤ S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S₁ : Subalgebra R A<VAR>S₂ : StarSubalgebra R A<GOAL>S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toSubalgebra
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>↑(StarAlgebra.adjoin R s) = ⋂ t, ⋂ (_ : Set.range ⇑(algebraMap R A) ⊆ ↑t ∧ s ⊆ ↑t ∧ star s ⊆ ↑t), ↑t
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>StarAlgebra.adjoin R s = (Algebra.adjoin R s).starClosure
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>(StarAlgebra.adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>s ⊆ ↑(StarAlgebra.adjoin R s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>star s ⊆ ↑(StarAlgebra.adjoin R s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ StarAlgebra.adjoin R {x}
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>x : A<GOAL>star x ∈ StarAlgebra.adjoin R {x}
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>GaloisConnection (StarAlgebra.adjoin R) SetLike.coe
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>s : Set A<VAR>hs : s ⊆ ↑S<GOAL>StarAlgebra.adjoin R s ≤ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>s : Set A<GOAL>StarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>StarAlgebra.adjoin R ↑S = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<GOAL>Subalgebra.toSubmodule (StarAlgebra.adjoin R s).toSubalgebra = Submodule.span R ↑(Submonoid.closure (s ∪ star s))
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Subalgebra R A<GOAL>S.starClosure = StarAlgebra.adjoin R ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<VAR>p : A → Prop<VAR>a : A<VAR>h : a ∈ StarAlgebra.adjoin R s<VAR>mem : ∀ x ∈ s, p x<VAR>algebraMap : ∀ (r : R), p ((algebraMap R A) r)<VAR>add : ∀ (x y : A), p x → p y → p (x + y)<VAR>mul : ∀ (x y : A), p x → p y → p (x * y)<VAR>star : ∀ (x : A), p x → p (star x)<GOAL>p a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ StarAlgebra.adjoin R s<VAR>hb : b ∈ StarAlgebra.adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hstar : ∀ (x y : A), p x y → p (star x) (star y)<VAR>Hstar_left : ∀ (x y : A), p x y → p (star x) y<VAR>Hstar_right : ∀ (x y : A), p x y → p x (star y)<GOAL>p a b
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>s : Set A<VAR>p : ↥(StarAlgebra.adjoin R s) → Prop<VAR>a : ↥(StarAlgebra.adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((algebraMap R ↥(StarAlgebra.adjoin R s)) r)<VAR>add : ∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(StarAlgebra.adjoin R s)), p x → p (star x)<GOAL>p a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>↑⊤ = Set.univ
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>⊤.toSubalgebra = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>S.toSubalgebra = ⊤ ↔ S = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<VAR>x : A<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<VAR>x : A<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>S T : StarSubalgebra R A<GOAL>StarSubalgebra.map f (S ⊔ T) = StarSubalgebra.map f S ⊔ StarSubalgebra.map f T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<VAR>x : A<GOAL>x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S T : StarSubalgebra R A<GOAL>(S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Set (StarSubalgebra R A)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Set (StarSubalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : Set (StarSubalgebra R A)<GOAL>(sInf S).toSubalgebra = sInf (StarSubalgebra.toSubalgebra '' S)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>ι : Sort u_5<VAR>S : ι → StarSubalgebra R A<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>ι : Sort u_5<VAR>S : ι → StarSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>ι : Sort u_5<VAR>S : ι → StarSubalgebra R A<GOAL>(⨅ i, S i).toSubalgebra = ⨅ i, (S i).toSubalgebra
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>⊥.toSubalgebra = ⊥
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>x : A<GOAL>x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<GOAL>↑⊥ = Set.range ⇑(algebraMap R A)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>S = ⊤ ↔ ∀ (x : A), x ∈ S
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>StarAlgHomClass F R A B<VAR>f g : F<VAR>x : A<GOAL>x ∈ StarAlgHom.equalizer f g ↔ f x = g x
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>StarAlgHomClass F R A B<VAR>f g : F<VAR>s : Set A<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>StarAlgebra.adjoin R s ≤ StarAlgHom.equalizer f g
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>StarAlgHomClass F R A B<VAR>s : Set A<VAR>h : StarAlgebra.adjoin R s = ⊤<VAR>f g : F<VAR>hs : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>s : Set A<GOAL>StarSubalgebra.map f (StarAlgebra.adjoin R s) = StarAlgebra.adjoin R (⇑f '' s)