ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>r : R<GOAL>φ ((algebraMap R A) r) = (algebraMap R B) r
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<GOAL>(↑φ).comp (algebraMap R A) = algebraMap R B
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>r s : A<GOAL>φ (r + s) = φ r + φ s
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<GOAL>φ 0 = 0
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>x y : A<GOAL>φ (x * y) = φ x * φ y
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<GOAL>φ 1 = 1
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>x : A<VAR>n : ℕ<GOAL>φ (x ^ n) = φ x ^ n
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>r : R<VAR>x : A<GOAL>φ (r • x) = r • φ x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>ι : Type u_1<VAR>f : ι → A<VAR>s : Finset ι<GOAL>φ (∑ x ∈ s, f x) = ∑ x ∈ s, φ (f x)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>α : Type u_1<VAR>Zero α<VAR>ι : Type u_2<VAR>f : ι →₀ α<VAR>g : ι → α → A<GOAL>φ (f.sum g) = f.sum fun i a => φ (g i a)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →+* B<VAR>h : ∀ (c : R) (x : A), f (c • x) = c • f x<GOAL>⇑(AlgHom.mk' f h) = ⇑f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⇑(AlgHom.id R A) = id
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑(AlgHom.id R A) = RingHom.id A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : A<GOAL>(AlgHom.id R A) p = p
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>φ₁ : B →ₐ[R] C<VAR>φ₂ : A →ₐ[R] B<GOAL>⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>φ₁ : B →ₐ[R] C<VAR>φ₂ : A →ₐ[R] B<VAR>p : A<GOAL>(φ₁.comp φ₂) p = φ₁ (φ₂ p)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>φ₁ : B →ₐ[R] C<VAR>φ₂ : A →ₐ[R] B<GOAL>↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<GOAL>φ.comp (AlgHom.id R A) = φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<GOAL>(AlgHom.id R B).comp φ = φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>D : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Semiring D<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>Algebra R D<VAR>φ₁ : C →ₐ[R] D<VAR>φ₂ : B →ₐ[R] C<VAR>φ₃ : A →ₐ[R] B<GOAL>(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>p : A<GOAL>φ.toLinearMap p = φ p
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>Function.Injective AlgHom.toLinearMap
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<GOAL>(g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>(AlgHom.id R A).toLinearMap = LinearMap.id
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<VAR>map_one : f 1 = 1<VAR>map_mul : ∀ (x y : A), f (x * y) = f x * f y<VAR>a : A<GOAL>(AlgHom.ofLinearMap f map_one map_mul) a = f a
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>map_one : φ.toLinearMap 1 = 1<VAR>map_mul : ∀ (x y : A), φ.toLinearMap (x * y) = φ.toLinearMap x * φ.toLinearMap y<GOAL>AlgHom.ofLinearMap φ.toLinearMap map_one map_mul = φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<VAR>map_one : f 1 = 1<VAR>map_mul : ∀ (x y : A), f (x * y) = f x * f y<GOAL>(AlgHom.ofLinearMap f map_one map_mul).toLinearMap = f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>map_one : LinearMap.id 1 = 1<VAR>map_mul : ∀ (x y : A), LinearMap.id (x * y) = LinearMap.id x * LinearMap.id y<GOAL>AlgHom.ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>R' : Type u_1<VAR>SMul R' A<VAR>SMul R' B<VAR>LinearMap.CompatibleSMul A B R' R<VAR>r : R'<VAR>x : A<GOAL>φ (r • x) = r • φ x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>s : List A<GOAL>φ s.prod = (List.map (⇑φ) s).prod
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>1 = AlgHom.id R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>φ₁ φ₂ : A →ₐ[R] A<GOAL>φ₁ * φ₂ = φ₁.comp φ₂
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>1 x = x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>φ ψ : A →ₐ[R] A<VAR>x : A<GOAL>(φ * ψ) x = φ (ψ x)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>y : R<VAR>x : A<VAR>h : (algebraMap R A) y = x<GOAL>(algebraMap R B) y = f x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>s : Multiset A<GOAL>φ s.prod = (Multiset.map (⇑φ) s).prod
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>ι : Type u_1<VAR>f : ι → A<VAR>s : Finset ι<GOAL>φ (∏ x ∈ s, f x) = ∏ x ∈ s, φ (f x)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>α : Type u_1<VAR>Zero α<VAR>ι : Type u_2<VAR>f : ι →₀ α<VAR>g : ι → α → A<GOAL>φ (f.prod g) = f.prod fun i a => φ (g i a)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>x : A<GOAL>φ (-x) = -φ x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>φ : A →ₐ[R] B<VAR>x y : A<GOAL>φ (x - y) = φ x - φ y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>Algebra ℤ R<VAR>Algebra ℤ S<GOAL>Function.Injective RingHom.toIntAlgHom
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(Algebra.ofId R A) r = (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>f g : R →ₐ[R] A<GOAL>f = g
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>f : A →ₐ[R] A<VAR>x : Aˣ<GOAL>f • x = (Units.map ↑f) x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submonoid R<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Submonoid.map f (Algebra.algebraMapSubmonoid A M) = Algebra.algebraMapSubmonoid B M
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>M : Submonoid R<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>Algebra.algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Algebra.algebraMapSubmonoid B M)
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Monoid M<VAR>MulSemiringAction M A<VAR>SMulCommClass M R A<VAR>m : M<VAR>a : A<GOAL>(MulSemiringAction.toAlgHom R A m) a = m • a
<VAR>M : Type u_1<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Monoid M<VAR>MulSemiringAction M A<VAR>SMulCommClass M R A<VAR>FaithfulSMul M A<GOAL>Function.Injective (MulSemiringAction.toAlgHom R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>RingHom.ker f.rangeRestrict = RingHom.ker f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommRing S<VAR>Algebra R S<VAR>S' : Subalgebra R S<VAR>ι : Type u_3<VAR>ι' : Finset ι<VAR>s l : ι → S<VAR>e : ∑ i ∈ ι', l i * s i = 1<VAR>hs : ∀ (i : ι), s i ∈ S'<VAR>hl : ∀ (i : ι), l i ∈ S'<VAR>x : S<VAR>H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'<GOAL>x ∈ S'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommRing S<VAR>Algebra R S<VAR>S' : Subalgebra R S<VAR>s : Set S<VAR>l : ↑s →₀ S<VAR>hs : (Finsupp.total (↑s) S S Subtype.val) l = 1<VAR>hs' : s ⊆ ↑S'<VAR>hl : ∀ (i : ↑s), l i ∈ S'<VAR>x : S<VAR>H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ S'<GOAL>x ∈ S'
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.op.toSubsemiring = S.op
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>↑S.op = MulOpposite.unop ⁻¹' ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : Aᵐᵒᵖ<VAR>S : Subalgebra R A<GOAL>x ∈ S.op ↔ MulOpposite.unop x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>S.unop.toSubsemiring = S.unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>↑S.unop = MulOpposite.op ⁻¹' ↑S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>x ∈ S.unop ↔ MulOpposite.op x ∈ S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.op.unop = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>S.unop.op = S
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ : Subalgebra R A<VAR>S₂ : Subalgebra R Aᵐᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ : Subalgebra R Aᵐᵒᵖ<VAR>S₂ : Subalgebra R A<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R A<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R Aᵐᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>(RelIso.symm Subalgebra.opEquiv) S = S.unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>Subalgebra.opEquiv S = S.op
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊥.op = ⊥
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊥.unop = ⊥
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊤.op = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊤.unop = ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R A<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R Aᵐᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R A<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S₁ S₂ : Subalgebra R Aᵐᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<GOAL>(sSup S).op = sSup (Subalgebra.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R Aᵐᵒᵖ)<GOAL>(sSup S).unop = sSup (Subalgebra.op ⁻¹' S)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R A)<GOAL>(sInf S).op = sInf (Subalgebra.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Set (Subalgebra R Aᵐᵒᵖ)<GOAL>(sInf S).unop = sInf (Subalgebra.op ⁻¹' S)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : ι → Subalgebra R A<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : ι → Subalgebra R Aᵐᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : ι → Subalgebra R A<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : ι → Subalgebra R Aᵐᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>(Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set Aᵐᵒᵖ<GOAL>(Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : ↥S.toSubsemiring), ↑(S.linearEquivOp a) = MulOpposite.op ↑a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : ↥S.op), ↑(S.linearEquivOp.symm a) = MulOpposite.unop ↑a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : (↥S.op)ᵐᵒᵖ), ↑(S.algEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : ↥S.toSubsemiring), S.algEquivOpMop a = MulOpposite.op (S.addEquivOp a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : ↥S.op), S.mopAlgEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>∀ (a : (↥S.toSubsemiring)ᵐᵒᵖ), ↑(S.mopAlgEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.op.toSubring = S.toSubring.op
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R Aᵐᵒᵖ<GOAL>S.unop.toSubring = S.toSubring.unop
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Algebra R A<VAR>r : R<VAR>x : A<GOAL>r • x = Algebra.toRingHom r * x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Algebra R A<VAR>r : R<VAR>x : A<GOAL>Algebra.toRingHom r * x = x * Algebra.toRingHom r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : ℕ<GOAL>↑↑a = ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a b : R<GOAL>↑(a + b) = ↑a + ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a b : R<GOAL>↑(a * b) = ↑a * ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : R<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>x : R<GOAL>↑(-x) = -↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a b : R<GOAL>↑(a - b) = ↑a - ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → R<GOAL>↑(∏ i ∈ s, a i) = ∏ i ∈ s, ↑(a i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → R<GOAL>↑(∑ i ∈ s, a i) = ∑ i ∈ s, ↑(a i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommSemiring S<VAR>i : R →+* S<GOAL>algebraMap R S = i
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>Semiring A<VAR>P Q : Algebra R A<VAR>h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r<GOAL>P = Q
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>x : A<GOAL>r • x = (algebraMap R A) r * x
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R A) r = r • 1
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⇑(algebraMap R A) = fun r => r • 1
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>x : A<GOAL>(algebraMap R A) r * x = x * (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>x : A<GOAL>Commute ((algebraMap R A) r) x
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>x : A<GOAL>Commute x ((algebraMap R A) r)
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>r : R<VAR>y : A<GOAL>x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<VAR>r : R<VAR>y : A<GOAL>x * (algebraMap R A) r * y = x * y * (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>RingHom.smulOneHom = algebraMap R A
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : R<VAR>x y : A<GOAL>x * s • y = s • (x * y)
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<VAR>x y : A<GOAL>r • x * y = r • (x * y)
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>α : Type u_2<VAR>Monoid α<VAR>MulDistribMulAction α A<VAR>SMulCommClass α R A<VAR>a : α<VAR>r : R<GOAL>a • (algebraMap R A) r = (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(Algebra.linearMap R A) r = (algebraMap R A) r
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⇑(Algebra.linearMap R A) = ⇑(algebraMap R A)
<VAR>R : Type u<VAR>CommSemiring R<GOAL>algebraMap R R = RingHom.id R
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>(algebraMap R R) x = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<GOAL>x • y = x * y
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>SMul A B<VAR>CommSemiring B<VAR>Semiring C<VAR>Algebra B C<VAR>SMul A C<VAR>IsScalarTower A B C<VAR>a : A<VAR>b : B<GOAL>↑(a • b) = a • ↑b
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ Set.range ⇑f = {0}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>Semiring β<VAR>f : α →+* β<VAR>a : α<GOAL>IsUnit a → IsUnit (f a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>Semiring β<VAR>f : α →+* β<VAR>a b : α<GOAL>a ∣ b → f a ∣ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Ring α<VAR>IsDomain α<VAR>Ring β<VAR>f : β →+* α<VAR>hf : Function.Injective ⇑f<GOAL>IsDomain β
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>Subalgebra.toSubmodule S * Subalgebra.toSubmodule T ≤ Subalgebra.toSubmodule (S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>Subalgebra.toSubmodule S * Subalgebra.toSubmodule S = Subalgebra.toSubmodule S
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>Subalgebra.toSubmodule S * Subalgebra.toSubmodule T = Subalgebra.toSubmodule (S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>R' : Type u_3<VAR>Semiring R'<VAR>MulSemiringAction R' A<VAR>SMulCommClass R' R A<VAR>m : R'<VAR>S : Subalgebra R A<GOAL>↑(m • S) = m • ↑S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>R' : Type u_3<VAR>Semiring R'<VAR>MulSemiringAction R' A<VAR>SMulCommClass R' R A<VAR>m : R'<VAR>S : Subalgebra R A<GOAL>(m • S).toSubsemiring = m • S.toSubsemiring
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>R' : Type u_3<VAR>Semiring R'<VAR>MulSemiringAction R' A<VAR>SMulCommClass R' R A<VAR>m : R'<VAR>S : Subalgebra R A<GOAL>Subalgebra.toSubmodule (m • S) = m • Subalgebra.toSubmodule S
<VAR>R' : Type u_4<VAR>R : Type u_5<VAR>A : Type u_6<VAR>Semiring R'<VAR>CommRing R<VAR>Ring A<VAR>MulSemiringAction R' A<VAR>Algebra R A<VAR>SMulCommClass R' R A<VAR>m : R'<VAR>S : Subalgebra R A<GOAL>(m • S).toSubring = m • S.toSubring
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>R' : Type u_3<VAR>Semiring R'<VAR>MulSemiringAction R' A<VAR>SMulCommClass R' R A<VAR>m : R'<VAR>r : A<VAR>S : Subalgebra R A<GOAL>r ∈ S → m • r ∈ m • S
<VAR>R : Type u<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>a : A<GOAL>⇑((Algebra.lsmul R B M) a) = fun x => a • x
<VAR>R : Type u<VAR>A : Type w<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>MulAction A M<VAR>SMul R M<VAR>IsScalarTower R A M<VAR>r : R<VAR>x : M<GOAL>(algebraMap R A) r • x = r • x
<VAR>R : Type u<VAR>A : Type w<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>MulAction A M<VAR>SMul R M<VAR>h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x<GOAL>IsScalarTower R A M
<VAR>R : Type u<VAR>A : Type w<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>MulAction A M<GOAL>IsScalarTower R A M
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)<GOAL>IsScalarTower R S A