ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>U : Type u_2<VAR>CommRing U<VAR>Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot U f<VAR>e : S ≃ₐ[R] T<GOAL>(h.ofEquiv e).aequiv h' = e.symm.trans (h.aequiv h')
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R[X]<VAR>IsDomain R<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>h : IsAdjoinRootMonic S f<VAR>hirr : Irreducible f<GOAL>minpoly R h.root = f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx' : IsIntegral R x<GOAL>minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen
<VAR>D : Type u_1<VAR>DivisionRing D<VAR>Finite D<VAR>hD : LittleWedderburn.InductionHyp D<GOAL>Subring.center D = ⊤
<VAR>D : Type u_1<VAR>DivisionRing D<VAR>Finite D<GOAL>Subring.center D = ⊤
<VAR>D : Type u_1<VAR>Finite D<VAR>Ring D<VAR>IsDomain D<GOAL>IsField D
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.IsRadical ↔ IsReduced (R ⧸ I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>hI : IsNilpotent I<VAR>P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop<VAR>h₁ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I<VAR>h₂ : ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (Ideal.map (Ideal.Quotient.mk I) J) → P J<GOAL>P I
<VAR>R : Type u_3<VAR>CommRing R<VAR>I : Ideal R<VAR>hI : IsNilpotent I<VAR>x : R<GOAL>IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_8<VAR>AddCommMonoid N<VAR>Module R N<GOAL>IsTensorProduct (TensorProduct.mk R M N)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>h : IsTensorProduct f<GOAL>∀ (a : M₁ ⊗[R] M₂), h.equiv a = (TensorProduct.lift f) a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>h : IsTensorProduct f<GOAL>↑h.equiv = TensorProduct.lift f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>h : IsTensorProduct f<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>Module R M'<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>h : IsTensorProduct f<VAR>f' : M₁ →ₗ[R] M₂ →ₗ[R] M'<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>(h.lift f') ((f x₁) x₂) = (f' x₁) x₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>N₁ : Type u_6<VAR>N₂ : Type u_7<VAR>N : Type u_8<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>AddCommMonoid N<VAR>Module R N₁<VAR>Module R N₂<VAR>Module R N<VAR>g : N₁ →ₗ[R] N₂ →ₗ[R] N<VAR>hf : IsTensorProduct f<VAR>hg : IsTensorProduct g<VAR>i₁ : M₁ →ₗ[R] N₁<VAR>i₂ : M₂ →ₗ[R] N₂<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>(hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>h : IsTensorProduct f<VAR>C : M → Prop<VAR>m : M<VAR>h0 : C 0<VAR>htmul : ∀ (x : M₁) (y : M₂), C ((f x) y)<VAR>hadd : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C m
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>Q : Type u_3<VAR>AddCommMonoid Q<VAR>Module S Q<VAR>Module R Q<VAR>IsScalarTower R S Q<VAR>g : M →ₗ[R] Q<VAR>x : M<GOAL>(h.lift g) (f x) = g x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>Q : Type u_3<VAR>AddCommMonoid Q<VAR>Module S Q<VAR>Module R Q<VAR>IsScalarTower R S Q<VAR>g : M →ₗ[R] Q<GOAL>↑R (h.lift g) ∘ₗ f = g
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>x : N<VAR>P : N → Prop<VAR>h₁ : P 0<VAR>h₂ : ∀ (m : M), P (f m)<VAR>h₃ : ∀ (s : S) (n : N), P n → P (s • n)<VAR>h₄ : ∀ (n₁ n₂ : N), P n₁ → P n₂ → P (n₁ + n₂)<GOAL>P x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>Q : Type u_3<VAR>AddCommMonoid Q<VAR>Module S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ∀ (x : M), g₁ (f x) = g₂ (f x)<GOAL>g₁ = g₂
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>Q : Type u_3<VAR>AddCommMonoid Q<VAR>Module S Q<VAR>Module R Q<VAR>IsScalarTower R S Q<VAR>g₁ g₂ : N →ₗ[S] Q<VAR>e : ↑R g₁ ∘ₗ f = ↑R g₂ ∘ₗ f<GOAL>g₁ = g₂
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<GOAL>IsBaseChange S ((TensorProduct.mk R S M) 1)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>s : S<VAR>m : M<GOAL>h.equiv (s ⊗ₜ[R] m) = s • f m
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>m : M<GOAL>h.equiv.symm (f m) = 1 ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g<GOAL>IsBaseChange S f
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<GOAL>IsBaseChange S f ↔ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>Module R M<VAR>Module R N<VAR>e : M ≃ₗ[R] N<GOAL>IsBaseChange R ↑e
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module R M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>T : Type u_4<VAR>O : Type u_5<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>AddCommMonoid O<VAR>Module R O<VAR>Module S O<VAR>Module T O<VAR>IsScalarTower S T O<VAR>IsScalarTower R S O<VAR>IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<GOAL>IsBaseChange T (↑R g ∘ₗ f)
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<GOAL>Algebra.IsPushout R S R' S' ↔ IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>self : Algebra.IsPushout R S R' S'<GOAL>IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>h : Algebra.IsPushout R S R' S'<GOAL>Algebra.IsPushout R R' S S'
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<GOAL>Algebra.IsPushout R S R' S' ↔ Algebra.IsPushout R R' S S'
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>H : Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>a : S'<GOAL>(Algebra.pushoutDesc S' f g hf) a = (⋯.lift g.toLinearMap) a
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>H : Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<GOAL>∀ (H_1 : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : S), (Algebra.pushoutDesc S' f g H_1) ((algebraMap S S') x) = f x
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<GOAL>(Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R S S') = f
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>H : Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<GOAL>∀ (H_1 : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : R'), (Algebra.pushoutDesc S' f g H_1) ((algebraMap R' S') x) = g x
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<GOAL>(Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R R' S') = g
<VAR>R : Type u_1<VAR>S : Type v₃<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>H : Algebra.IsPushout R S R' S'<VAR>A : Type u_8<VAR>Semiring A<VAR>Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (IsScalarTower.toAlgHom R R' S') = g.comp (IsScalarTower.toAlgHom R R' S')<VAR>h₂ : f.comp (IsScalarTower.toAlgHom R S S') = g.comp (IsScalarTower.toAlgHom R S S')<GOAL>f = g
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoidWithOne (A i)<VAR>(i : ι) → Module R (A i)<GOAL>1 = (PiTensorProduct.tprod R) 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y : (i : ι) → A i<GOAL>(PiTensorProduct.mul ((PiTensorProduct.tprod R) x)) ((PiTensorProduct.tprod R) y) = (PiTensorProduct.tprod R) (x * y)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y : ⨂[R] (i : ι), A i<GOAL>x * y = (PiTensorProduct.mul x) y
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y : (i : ι) → A i<GOAL>(PiTensorProduct.tprod R) x * (PiTensorProduct.tprod R) y = (PiTensorProduct.tprod R) (x * y)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>a₁ a₂ a₃ : (i : ι) → A i<VAR>ha : SemiconjBy a₁ a₂ a₃<GOAL>SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>a₁ a₂ : (i : ι) → A i<VAR>ha : Commute a₁ a₂<GOAL>Commute ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>r s : R<VAR>x y : (i : ι) → A i<GOAL>r • (PiTensorProduct.tprod R) x * s • (PiTensorProduct.tprod R) y = (r * s) • (PiTensorProduct.tprod R) (x * y)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x : ⨂[R] (i : ι), A i<GOAL>(PiTensorProduct.mul ((PiTensorProduct.tprod R) 1)) x = x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x : ⨂[R] (i : ι), A i<GOAL>(PiTensorProduct.mul x) ((PiTensorProduct.tprod R) 1) = x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonAssocSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>a : (i : ι) → A i<GOAL>(PiTensorProduct.tprodMonoidHom R) a = (PiTensorProduct.tprod R) a
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → NonUnitalSemiring (A i)<VAR>(i : ι) → Module R (A i)<VAR>∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x y z : ⨂[R] (i : ι), A i<GOAL>(PiTensorProduct.mul ((PiTensorProduct.mul x) y)) z = (PiTensorProduct.mul x) ((PiTensorProduct.mul y) z)
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R'<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>Algebra R' R<VAR>(i : ι) → Algebra R (A i)<VAR>(i : ι) → Algebra R' (A i)<VAR>∀ (i : ι), IsScalarTower R' R (A i)<VAR>r : R'<VAR>i : ι<VAR>DecidableEq ι<GOAL>(algebraMap R' (⨂[R] (i : ι), A i)) r = (PiTensorProduct.tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>DecidableEq ι<VAR>i : ι<VAR>a : A i<GOAL>(PiTensorProduct.singleAlgHom i) a = (PiTensorProduct.tprod R) ((MonoidHom.mulSingle A i) a)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>S : Type u_5<VAR>Semiring S<VAR>Algebra R S<VAR>f : MultilinearMap R A S<VAR>one : f 1 = 1<VAR>mul : ∀ (x y : (i : ι) → A i), f (x * y) = f x * f y<VAR>a : ⨂[R] (i : ι), A i<GOAL>(PiTensorProduct.liftAlgHom f one mul) a = (PiTensorProduct.lift f) a
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>κ : Type u_5<VAR>s : Finset κ<VAR>x : κ → (i : ι) → A i<VAR>hx : (↑s).Pairwise fun a b => Commute (x a) (x b)<GOAL>(PiTensorProduct.tprod R) (s.noncommProd x hx) = s.noncommProd (fun k => (PiTensorProduct.tprod R) (x k)) ⋯
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → Semiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>S : Type u_5<VAR>Finite ι<VAR>DecidableEq ι<VAR>Semiring S<VAR>Algebra R S<VAR>f g : (⨂[R] (i : ι), A i) →ₐ[R] S<VAR>h : ∀ (i : ι), f.comp (PiTensorProduct.singleAlgHom i) = g.comp (PiTensorProduct.singleAlgHom i)<GOAL>f = g
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → CommSemiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>x y : ⨂[R] (i : ι), A i<GOAL>(PiTensorProduct.mul x) y = (PiTensorProduct.mul y) x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>CommSemiring R<VAR>(i : ι) → CommSemiring (A i)<VAR>(i : ι) → Algebra R (A i)<VAR>κ : Type u_5<VAR>s : Finset κ<VAR>x : κ → (i : ι) → A i<GOAL>(PiTensorProduct.tprod R) (∏ k ∈ s, x k) = ∏ k ∈ s, (PiTensorProduct.tprod R) (x k)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Fintype ι<VAR>x : ι → R<GOAL>(PiTensorProduct.constantBaseRingEquiv ι R) ((PiTensorProduct.tprod R) x) = ∏ i : ι, x i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Fintype ι<VAR>r : R<GOAL>(PiTensorProduct.constantBaseRingEquiv ι R).symm r = (algebraMap R (⨂[R] (x : ι), R)) r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<GOAL>∏ k ∈ Finset.range n, (1 - μ ^ (k + 1)) = ↑n + 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ (n + 1)<GOAL>(-1) ^ n * ∏ k ∈ Finset.range n, (μ ^ (k + 1) - 1) = ↑n + 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>k n : ℕ<VAR>hn : k < n<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<GOAL>∃ z ∈ Algebra.adjoin ℤ {μ}, ↑n = z * (μ - 1) ^ k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.weightedTotalDegree' w p = ⊥ ↔ p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>w : σ → M<GOAL>MvPolynomial.weightedTotalDegree' w 0 = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : p ≠ 0<GOAL>MvPolynomial.weightedTotalDegree' w p = ↑(MvPolynomial.weightedTotalDegree w p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>OrderBot M<VAR>w : σ → M<GOAL>MvPolynomial.weightedTotalDegree w 0 = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>OrderBot M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(Finsupp.weight w) d ≤ MvPolynomial.weightedTotalDegree w φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>p : MvPolynomial σ R<GOAL>p ∈ MvPolynomial.weightedHomogeneousSubmodule R w m ↔ MvPolynomial.IsWeightedHomogeneous w p m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m : M<GOAL>MvPolynomial.weightedHomogeneousSubmodule R w m = Finsupp.supported R R {d | (Finsupp.weight w) d = m}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m n : M<GOAL>MvPolynomial.weightedHomogeneousSubmodule R w m * MvPolynomial.weightedHomogeneousSubmodule R w n ≤ MvPolynomial.weightedHomogeneousSubmodule R w (m + n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>d : σ →₀ ℕ<VAR>r : R<VAR>m : M<VAR>hm : (Finsupp.weight w) d = m<GOAL>MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.monomial d) r) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>SemilatticeSup M<VAR>OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : MvPolynomial.weightedTotalDegree w p = ⊥<GOAL>MvPolynomial.IsWeightedHomogeneous w p ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>r : R<GOAL>MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.C r) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m : M<GOAL>MvPolynomial.IsWeightedHomogeneous w 0 m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<GOAL>MvPolynomial.IsWeightedHomogeneous w 1 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>i : σ<GOAL>MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.X i) (w i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>φ : MvPolynomial σ R<VAR>n : M<VAR>w : σ → M<VAR>hφ : MvPolynomial.IsWeightedHomogeneous w φ n<VAR>d : σ →₀ ℕ<VAR>hd : (Finsupp.weight w) d ≠ n<GOAL>MvPolynomial.coeff d φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>φ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : φ ≠ 0<VAR>hm : MvPolynomial.IsWeightedHomogeneous w φ m<VAR>hn : MvPolynomial.IsWeightedHomogeneous w φ n<GOAL>m = n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>n : M<VAR>w : σ → M<VAR>hφ : MvPolynomial.IsWeightedHomogeneous w φ n<VAR>hψ : MvPolynomial.IsWeightedHomogeneous w ψ n<GOAL>MvPolynomial.IsWeightedHomogeneous w (φ + ψ) n