ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>φ ψ : F<VAR>x : A<GOAL>x ∈ NonUnitalAlgHom.equalizer φ ψ ↔ φ x = ψ x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<GOAL>(NonUnitalAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(NonUnitalSubsemiring.closure s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<GOAL>s ⊆ ↑(NonUnitalAlgebra.adjoin R s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : A<GOAL>x ∈ NonUnitalAlgebra.adjoin R {x}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>p : A → Prop<VAR>a : A<VAR>h : a ∈ NonUnitalAlgebra.adjoin R s<VAR>mem : ∀ x ∈ s, p x<VAR>add : ∀ (x y : A), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : A), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : A), p x → p (r • x)<GOAL>p a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ NonUnitalAlgebra.adjoin R s<VAR>hb : b ∈ NonUnitalAlgebra.adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H0_left : ∀ (y : A), p 0 y<VAR>H0_right : ∀ (x : A), p x 0<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>Hsmul_left : ∀ (r : R) (x y : A), p x y → p (r • x) y<VAR>Hsmul_right : ∀ (r : R) (x y : A), p x y → p x (r • y)<GOAL>p a b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>p : ↥(NonUnitalAlgebra.adjoin R s) → Prop<VAR>a : ↥(NonUnitalAlgebra.adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(NonUnitalAlgebra.adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(NonUnitalAlgebra.adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(NonUnitalAlgebra.adjoin R s)), p x → p (r • x)<GOAL>p a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>p : (x : A) → x ∈ NonUnitalAlgebra.adjoin R s → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p x ⋯<VAR>add : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>zero : p 0 ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯<VAR>smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx → p (r • x) ⋯<VAR>a : A<VAR>ha : a ∈ NonUnitalAlgebra.adjoin R s<GOAL>p a ha
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>GaloisConnection (NonUnitalAlgebra.adjoin R) SetLike.coe
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<VAR>s : Set A<VAR>hs : s ⊆ ↑S<GOAL>NonUnitalAlgebra.adjoin R s ≤ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<VAR>s : Set A<GOAL>NonUnitalAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s t : Set A<GOAL>NonUnitalAlgebra.adjoin R (s ∪ t) = NonUnitalAlgebra.adjoin R s ⊔ NonUnitalAlgebra.adjoin R t
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : NonUnitalSubalgebra R A<GOAL>NonUnitalAlgebra.adjoin R ↑s = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<GOAL>(NonUnitalAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>s : NonUnitalSubalgebra R A<GOAL>Submodule.span R ↑s = s.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalAlgebra.adjoin R ∅ = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalAlgebra.adjoin R Set.univ = ⊤
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>s : Set A<GOAL>NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (⇑f '' s)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>x : A<GOAL>NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R {x}) = NonUnitalAlgebra.adjoin R {f x}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : A<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>⊤.toSubmodule = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>⊤.toNonUnitalSubsemiring = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>NonUnitalNonAssocRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>⊤.toNonUnitalSubring = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.toSubmodule = ⊤ ↔ S = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.toNonUnitalSubring = ⊤ ↔ S = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>x y : A<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>S T : NonUnitalSubalgebra R A<GOAL>NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra 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>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<GOAL>(S ⊓ T).toSubmodule = S.toSubmodule ⊓ T.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<GOAL>(S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : Set (NonUnitalSubalgebra R A)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : Set (NonUnitalSubalgebra 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>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : Set (NonUnitalSubalgebra R A)<GOAL>(sInf S).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : Set (NonUnitalSubalgebra R A)<GOAL>(sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubalgebra R A<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubalgebra R A<GOAL>(⨅ i, S i).toSubmodule = ⨅ i, (S i).toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : A<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>⊥.toSubmodule = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<GOAL>S = ⊤ ↔ ∀ (x : A), x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>f : A →ₙₐ[R] B<GOAL>NonUnitalAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalAlgHom.range (NonUnitalAlgHom.id R A) = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>f : A →ₙₐ[R] B<GOAL>NonUnitalSubalgebra.map f ⊤ = NonUnitalAlgHom.range f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>f : A →ₙₐ[R] B<GOAL>NonUnitalSubalgebra.map f ⊥ = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>f : A →ₙₐ[R] B<GOAL>NonUnitalSubalgebra.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S ≤ T<GOAL>Function.Injective ⇑(NonUnitalSubalgebra.inclusion h)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S : NonUnitalSubalgebra R A<GOAL>NonUnitalSubalgebra.inclusion ⋯ = NonUnitalAlgHom.id R ↥S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S ≤ T<VAR>x : A<VAR>hx : x ∈ S<GOAL>(NonUnitalSubalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S ≤ T<VAR>x : ↥T<VAR>m : ↑x ∈ S<GOAL>(NonUnitalSubalgebra.inclusion h) ⟨↑x, m⟩ = x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T U : NonUnitalSubalgebra R A<VAR>hst : S ≤ T<VAR>htu : T ≤ U<VAR>x : ↥S<GOAL>(NonUnitalSubalgebra.inclusion htu) ((NonUnitalSubalgebra.inclusion hst) x) = (NonUnitalSubalgebra.inclusion ⋯) x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S ≤ T<VAR>s : ↥S<GOAL>↑((NonUnitalSubalgebra.inclusion h) s) = ↑s
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>S : NonUnitalSubalgebra R A<VAR>S₁ : NonUnitalSubalgebra R B<GOAL>↑(S.prod S₁) = ↑S ×ˢ ↑S₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>S : NonUnitalSubalgebra R A<VAR>S₁ : NonUnitalSubalgebra R B<GOAL>(S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>S : NonUnitalSubalgebra R A<VAR>S₁ : NonUnitalSubalgebra R B<VAR>x : A × B<GOAL>x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>S T : NonUnitalSubalgebra R A<VAR>S₁ T₁ : NonUnitalSubalgebra R B<GOAL>S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>IsScalarTower R B B<VAR>SMulCommClass R B B<VAR>S T : NonUnitalSubalgebra R A<VAR>S₁ T₁ : NonUnitalSubalgebra R B<GOAL>S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>S : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(iSup S) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)<VAR>T : NonUnitalSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ T<GOAL>(NonUnitalSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalSubalgebra.inclusion h) x) = (f i) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)<VAR>T : NonUnitalSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>h : K i ≤ T<GOAL>(NonUnitalSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalSubalgebra.inclusion h) = f i
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)<VAR>T : NonUnitalSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>hx : ↑x ∈ T<GOAL>(NonUnitalSubalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)<VAR>T : NonUnitalSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥T<VAR>hx : ↑x ∈ K i<GOAL>(NonUnitalSubalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>r : R<VAR>a : A<VAR>ha : a ∈ Set.center A<GOAL>r • a ∈ Set.center A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>↑(NonUnitalSubalgebra.center R A) = Set.center A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>(NonUnitalSubalgebra.center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>(NonUnitalSubalgebra.center R A).toNonUnitalSubring = NonUnitalSubring.center A
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_3<VAR>NonUnitalCommSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalSubalgebra.center R A = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a : A<GOAL>a ∈ NonUnitalSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>r : R<VAR>a : A<VAR>ha : a ∈ s.centralizer<GOAL>r • a ∈ s.centralizer
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<GOAL>↑(NonUnitalSubalgebra.centralizer R s) = s.centralizer
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s : Set A<VAR>z : A<GOAL>z ∈ NonUnitalSubalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>s t : Set A<VAR>h : s ⊆ t<GOAL>NonUnitalSubalgebra.centralizer R t ≤ NonUnitalSubalgebra.centralizer R s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>NonUnitalSubalgebra.centralizer R Set.univ = NonUnitalSubalgebra.center R A
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>x : R<VAR>S : NonUnitalSubsemiring R<GOAL>x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>x : R<VAR>S : NonUnitalSubring R<GOAL>x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S
<VAR>R : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>a : R<VAR>l : List R<VAR>h : ∀ b ∈ l, Commute a b<GOAL>Commute a l.sum
<VAR>R : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>b : R<VAR>l : List R<VAR>h : ∀ a ∈ l, Commute a b<GOAL>Commute l.sum b
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>HasDistribNeg M<VAR>l : List M<GOAL>(List.map Neg.neg l).prod = (-1) ^ l.length * l.prod
<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>l : List M₀<GOAL>0 ∈ l → l.prod = 0
<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>Nontrivial M₀<VAR>NoZeroDivisors M₀<VAR>l : List M₀<GOAL>l.prod = 0 ↔ 0 ∈ l
<VAR>M₀ : Type u_4<VAR>MonoidWithZero M₀<VAR>l : List M₀<VAR>Nontrivial M₀<VAR>NoZeroDivisors M₀<VAR>hL : 0 ∉ l<GOAL>l.prod ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>l : List ι<VAR>f : ι → R<VAR>r : R<GOAL>(List.map (fun b => r * f b) l).sum = r * (List.map f l).sum
<VAR>ι : Type u_1<VAR>R : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>l : List ι<VAR>f : ι → R<VAR>r : R<GOAL>(List.map (fun b => f b * r) l).sum = (List.map f l).sum * r
<VAR>R : Type u_5<VAR>NonUnitalSemiring R<VAR>a : R<VAR>l : List R<VAR>h : ∀ x ∈ l, a ∣ x<GOAL>a ∣ l.sum
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>f : ι → κ → R<VAR>a : R<VAR>l₁ : List ι<VAR>l₂ : List κ<GOAL>(List.zipWith (fun i j => a * f i j) l₁ l₂).sum = a * (List.zipWith f l₁ l₂).sum
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>HasDistribNeg α<VAR>s : Multiset α<GOAL>(Multiset.map Neg.neg s).prod = (-1) ^ Multiset.card s * s.prod
<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>s : Multiset α<VAR>h : 0 ∈ s<GOAL>s.prod = 0
<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>s : Multiset α<GOAL>s.prod = 0 ↔ 0 ∈ s