ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>f : α → M<GOAL>s.mulIndicator f * sᶜ.mulIndicator f = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f g : α → M<VAR>h : Disjoint (Function.mulSupport f) (Function.mulSupport g)<GOAL>(Function.mulSupport f).mulIndicator (f * g) = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>f g : α → M<VAR>h : Disjoint (Function.support f) (Function.support g)<GOAL>(Function.support f).indicator (f + g) = f
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>f g : α → M<VAR>h : Disjoint (Function.mulSupport f) (Function.mulSupport g)<GOAL>(Function.mulSupport g).mulIndicator (f * g) = g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>f g : α → M<VAR>h : Disjoint (Function.support f) (Function.support g)<GOAL>(Function.support g).indicator (f + g) = g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>f g : α → M<GOAL>s.indicator f + sᶜ.indicator g = s.piecewise f g
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>f g : α → M<GOAL>s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f : α → G<GOAL>s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f : α → G<GOAL>s.indicator (-f) = -s.indicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f : α → G<GOAL>(s.indicator fun a => -f a) = fun a => -s.indicator f a
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f : α → G<GOAL>(s.mulIndicator fun a => (f a)⁻¹) = fun a => (s.mulIndicator f a)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f g : α → G<GOAL>(s.indicator fun a => f a - g a) = fun a => s.indicator f a - s.indicator g a
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f g : α → G<GOAL>(s.mulIndicator fun a => f a / g a) = fun a => s.mulIndicator f a / s.mulIndicator g a
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f g : α → G<GOAL>s.indicator (f - g) = s.indicator f - s.indicator g
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f g : α → G<GOAL>s.mulIndicator (f / g) = s.mulIndicator f / s.mulIndicator g
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f : α → G<GOAL>sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f : α → G<GOAL>sᶜ.indicator f = f + -s.indicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s : Set α<VAR>f : α → G<GOAL>sᶜ.indicator f = f - s.indicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s : Set α<VAR>f : α → G<GOAL>sᶜ.mulIndicator f = f / s.mulIndicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).indicator f = t.indicator f + -s.indicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>Group G<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
<VAR>α : Type u_1<VAR>G : Type u_6<VAR>AddGroup G<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).indicator f = t.indicator f - s.indicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_6<VAR>AddGroup G<VAR>g : G → β<VAR>hg : ∀ (x : G), g (-x) = g x<VAR>s t : Set α<VAR>f : α → G<VAR>x : α<GOAL>g ((symmDiff s t).indicator f x) = g (s.indicator f x - t.indicator f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_6<VAR>Group G<VAR>g : G → β<VAR>hg : ∀ (x : G), g x⁻¹ = g x<VAR>s t : Set α<VAR>f : α → G<VAR>x : α<GOAL>g ((symmDiff s t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
<VAR>α : Type u_1<VAR>M : Type u_6<VAR>N : Type u_7<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>s : Set α<VAR>g : α → M<VAR>x : α<GOAL>f (s.indicator g x) = s.indicator (⇑f ∘ g) x
<VAR>α : Type u_1<VAR>M : Type u_6<VAR>N : Type u_7<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<VAR>s : Set α<VAR>g : α → M<VAR>x : α<GOAL>f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>c : R<GOAL>(algebraMap R Aᵐᵒᵖ) c = MulOpposite.op ((algebraMap R A) c)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>∀ (a : A), (AlgEquiv.opOp R A) a = MulOpposite.op (MulOpposite.op a)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>∀ (a : Aᵐᵒᵖᵐᵒᵖ), (AlgEquiv.opOp R A).symm a = MulOpposite.unop (MulOpposite.unop a)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>↑(AlgEquiv.opOp R A) = RingEquiv.opOp A
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>(f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>↑(f.fromOpposite hf) = (↑f).fromOpposite hf
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>(f.toOpposite hf).toLinearMap = ↑(MulOpposite.opLinearEquiv R) ∘ₗ f.toLinearMap
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : ∀ (x y : A), Commute (f x) (f y)<GOAL>↑(f.toOpposite hf) = (↑f).toOpposite hf
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>∀ (a : Aᵐᵒᵖ), (AlgHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ<GOAL>∀ (a : A), (AlgHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>(AlgHom.op f).toRingHom = RingHom.op f.toRingHom
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ<GOAL>(AlgHom.unop f).toRingHom = RingHom.unop f.toRingHom
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : Aᵐᵒᵖ →ₐ[R] B) (a_1 : A), (AlgHom.opComm.symm a) a_1 = MulOpposite.op (a (MulOpposite.op a_1))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : A →ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), (AlgHom.opComm a) a_1 = MulOpposite.unop (a (MulOpposite.unop a_1))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>∀ (a : Aᵐᵒᵖ), (AlgEquiv.op f) a = MulOpposite.op (f (MulOpposite.unop a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ<GOAL>∀ (a : A), (AlgEquiv.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>∀ (a : Bᵐᵒᵖ), (AlgEquiv.op f).symm a = MulOpposite.op ((↑↑f).symm (MulOpposite.unop a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ<GOAL>∀ (a : B), (AlgEquiv.op.symm f).symm a = MulOpposite.unop ((↑↑f).symm (MulOpposite.op a))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>↑(AlgEquiv.op f) = AlgHom.op ↑f
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<GOAL>(AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ<GOAL>↑(AlgEquiv.unop f) = AlgHom.unop ↑f
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ<GOAL>(AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), (AlgEquiv.opComm a) a_1 = MulOpposite.unop (a (MulOpposite.unop a_1))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : Bᵐᵒᵖ), (AlgEquiv.opComm.symm a).symm a_1 = MulOpposite.unop ((↑↑(AlgEquiv.refl.trans (a.trans (AlgEquiv.opOp R B)))).symm (MulOpposite.op a_1))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : B), (AlgEquiv.opComm a).symm a_1 = (↑↑AlgEquiv.refl).symm ((↑↑((AlgEquiv.op a).trans (AlgEquiv.opOp R B).symm)).symm a_1)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<GOAL>∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : A), (AlgEquiv.opComm.symm a) a_1 = MulOpposite.op (a (MulOpposite.op a_1))
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<GOAL>∀ (a : A), (AlgEquiv.toOpposite R A) a = MulOpposite.op a
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<GOAL>∀ (a : Aᵐᵒᵖ), (AlgEquiv.toOpposite R A).symm a = MulOpposite.unop a
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<GOAL>↑(AlgEquiv.toOpposite R A) = RingEquiv.toOpposite A
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<GOAL>(AlgEquiv.toOpposite R A).toLinearEquiv = MulOpposite.opLinearEquiv R
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : R<GOAL>(Algebra.lmul R A) ((algebraMap R A) x) = (Algebra.lsmul R R A) x
<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>IsScalarTower R S A<VAR>U : Subalgebra S A<GOAL>↑(Subalgebra.restrictScalars R U) = ↑U
<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>IsScalarTower R S A<GOAL>Subalgebra.restrictScalars R ⊤ = ⊤
<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>IsScalarTower R S A<VAR>U : Subalgebra S A<GOAL>Subalgebra.toSubmodule (Subalgebra.restrictScalars R U) = Submodule.restrictScalars R (Subalgebra.toSubmodule U)
<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>IsScalarTower R S A<VAR>U : Subalgebra S A<VAR>x : A<GOAL>x ∈ Subalgebra.restrictScalars R U ↔ x ∈ U
<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>IsScalarTower R S A<GOAL>Function.Injective (Subalgebra.restrictScalars R)
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>LinearMap.range (IsScalarTower.toAlgHom R (↥S) A) = Subalgebra.toSubmodule S
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>t : Set A<GOAL>Subalgebra.restrictScalars R (Algebra.adjoin (↥(IsScalarTower.toAlgHom R S A).range) t) = Subalgebra.restrictScalars R (Algebra.adjoin S t)
<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>S : Subalgebra R A<VAR>S₁ : Subalgebra R B<GOAL>↑(S.prod S₁) = ↑S ×ˢ ↑S₁
<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>S : Subalgebra R A<VAR>S₁ : Subalgebra R B<GOAL>Subalgebra.toSubmodule (S.prod S₁) = (Subalgebra.toSubmodule S).prod (Subalgebra.toSubmodule S₁)
<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>S : Subalgebra R A<VAR>S₁ : Subalgebra R B<VAR>x : A × B<GOAL>x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
<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<GOAL>⊤.prod ⊤ = ⊤
<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>S T : Subalgebra R A<VAR>S₁ T₁ : Subalgebra R B<GOAL>S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
<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>S T : Subalgebra R A<VAR>S₁ T₁ : Subalgebra R B<GOAL>S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
<VAR>I : Type u<VAR>R : Type u_1<VAR>f : I → Type v<GOAL>∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R), (algebraMap R ((i : I) → f i)) a = fun i => (algebraMap R (f i)) a
<VAR>I : Type u<VAR>R : Type u_1<VAR>f : I → Type v<GOAL>∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R) (i : I), (algebraMap R ((i : I) → f i)) a i = (algebraMap R (f i)) a
<VAR>I : Type u<VAR>R : Type u_1<VAR>f : I → Type v<GOAL>∀ {x : CommSemiring R} [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → Algebra R (f i)] (i : I) (f_1 : (i : I) → f i), (Pi.evalAlgHom R f i) f_1 = f_1 i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring B<VAR>Algebra R B<VAR>a : B<GOAL>∀ (a_1 : A), (Pi.constAlgHom R A B) a a_1 = Function.const A a a_1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<GOAL>Pi.constRingHom A R = algebraMap R (A → R)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<GOAL>Pi.constAlgHom R A R = Algebra.ofId R (A → 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>f : A →ₐ[R] B<VAR>I : Type u_2<VAR>h : I → A<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A₁ : ι → Type u_3<VAR>A₂ : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A₁ i)<VAR>(i : ι) → Semiring (A₂ i)<VAR>(i : ι) → Algebra R (A₁ i)<VAR>(i : ι) → Algebra R (A₂ i)<VAR>e : (i : ι) → A₁ i ≃ₐ[R] A₂ i<VAR>x : (i : ι) → A₁ i<VAR>j : ι<GOAL>(AlgEquiv.piCongrRight e) x j = (e j) (x j)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : ι → Type u_3<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>(i : ι) → Algebra R (A i)<GOAL>(AlgEquiv.piCongrRight fun i => AlgEquiv.refl) = AlgEquiv.refl
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A₁ : ι → Type u_3<VAR>A₂ : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A₁ i)<VAR>(i : ι) → Semiring (A₂ i)<VAR>(i : ι) → Algebra R (A₁ i)<VAR>(i : ι) → Algebra R (A₂ i)<VAR>e : (i : ι) → A₁ i ≃ₐ[R] A₂ i<GOAL>(AlgEquiv.piCongrRight e).symm = AlgEquiv.piCongrRight fun i => (e i).symm
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A₁ : ι → Type u_3<VAR>A₂ : ι → Type u_4<VAR>A₃ : ι → Type u_5<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A₁ i)<VAR>(i : ι) → Semiring (A₂ i)<VAR>(i : ι) → Semiring (A₃ i)<VAR>(i : ι) → Algebra R (A₁ i)<VAR>(i : ι) → Algebra R (A₂ i)<VAR>(i : ι) → Algebra R (A₃ i)<VAR>e₁ : (i : ι) → A₁ i ≃ₐ[R] A₂ i<VAR>e₂ : (i : ι) → A₂ i ≃ₐ[R] A₃ i<GOAL>(AlgEquiv.piCongrRight e₁).trans (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun i => (e₁ i).trans (e₂ i)
<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>r : R<GOAL>(algebraMap R (A × B)) r = ((algebraMap R A) r, (algebraMap R B) r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : A →ₐ[R] C<VAR>x : A<GOAL>(f.prod g) x = (f x, g x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : A →ₐ[R] C<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : A →ₐ[R] C<GOAL>(AlgHom.fst R B C).comp (f.prod g) = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : A →ₐ[R] C<GOAL>(AlgHom.snd R B C).comp (f.prod g) = g
<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<GOAL>(AlgHom.fst R A B).prod (AlgHom.snd R A B) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₐ[R] B × C<GOAL>AlgHom.prodEquiv.symm f = ((AlgHom.fst R B C).comp f, (AlgHom.snd R B C).comp f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>f : (A →ₐ[R] B) × (A →ₐ[R] C)<GOAL>AlgHom.prodEquiv f = f.1.prod f.2
<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>self : A →ₐ[R] B<VAR>r : R<GOAL>(↑↑self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>A : outParam (Type u_3)<VAR>B : outParam (Type u_4)<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>FunLike F A B<VAR>self : AlgHomClass F R A B<VAR>f : F<VAR>r : R<GOAL>f ((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>F : Type u_1<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<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<GOAL>(↑↑f.toRingHom).toFun = ⇑f
<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 : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r<GOAL>⇑{ toRingHom := f, commutes' := h } = ⇑f
<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₁ : f 1 = 1<VAR>h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y<VAR>h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0<VAR>h₄ : ∀ (x y : A), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y<VAR>h₅ : ∀ (r : R), (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r<GOAL>⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
<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 : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r<GOAL>↑{ toRingHom := f, commutes' := h } = f
<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<GOAL>f.toRingHom = ↑f
<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<GOAL>⇑↑f = ⇑f
<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 DFunLike.coe
<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>⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
<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 RingHomClass.toRingHom
<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 MonoidHomClass.toMonoidHom
<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 AddMonoidHomClass.toAddMonoidHom
<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>H : φ₁ = φ₂<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>φ : A →ₐ[R] B<VAR>x y : A<VAR>h : x = y<GOAL>φ 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<VAR>H : ∀ (x : A), φ₁ x = φ₂ x<GOAL>φ₁ = φ₂
<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>φ₁ = φ₂ ↔ ∀ (x : A), φ₁ 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>h₁ : f 1 = 1<VAR>h₂ : ∀ (x y : A), { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y<VAR>h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0<VAR>h₄ : ∀ (x y : A), (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y<VAR>h₅ : ∀ (r : R), (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r<GOAL>{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f