ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g h : M →ₗ[R] M<GOAL>(LinearMap.trace R M) (f * g * h) = (LinearMap.trace R M) (h * f * g)
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g h : M →ₗ[R] M<GOAL>(LinearMap.trace R M) (f * (g * h)) = (LinearMap.trace R M) (h * (f * g))
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>g : M →ₗ[R] M<VAR>f : (M →ₗ[R] M)ˣ<GOAL>(LinearMap.trace R M) (↑f * g * ↑f⁻¹) = (LinearMap.trace R M) g
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f g : Module.End R M<GOAL>(LinearMap.trace R M) ⁅f, g⁆ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_5<VAR>Finite ι<VAR>b : Basis ι R M<GOAL>LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_5<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<GOAL>LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>x : TensorProduct R (Module.Dual R M) M<GOAL>(LinearMap.trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>(LinearMap.trace R M) 1 = ↑(FiniteDimensional.finrank R M)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>(LinearMap.trace R M) LinearMap.id = ↑(FiniteDimensional.finrank R M)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>LinearMap.trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = LinearMap.trace R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<GOAL>LinearMap.trace R (M × N) ∘ₗ LinearMap.prodMapLinear R M N M N R = LinearMap.id.coprod LinearMap.id ∘ₗ (LinearMap.trace R M).prodMap (LinearMap.trace R N)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<GOAL>(LinearMap.trace R (M × N)) (f.prodMap g) = (LinearMap.trace R M) f + (LinearMap.trace R N) g
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<GOAL>(TensorProduct.mapBilinear R M N M N).compr₂ (LinearMap.trace R (TensorProduct R M N)) = (LinearMap.lsmul R R).compl₁₂ (LinearMap.trace R M) (LinearMap.trace R N)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<GOAL>(LinearMap.llcomp R M N M).compr₂ (LinearMap.trace R M) = (LinearMap.llcomp R N M N).flip.compr₂ (LinearMap.trace R N)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>(LinearMap.trace R (Module.Dual R M)) (Module.Dual.transpose f) = (LinearMap.trace R M) f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<GOAL>(LinearMap.trace R (TensorProduct R M N)) (TensorProduct.map f g) = (LinearMap.trace R M) f * (LinearMap.trace R N) g
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<GOAL>(LinearMap.trace R M) (g ∘ₗ f) = (LinearMap.trace R N) (f ∘ₗ g)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup P<VAR>Module R P<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>Module.Free R P<VAR>Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : P →ₗ[R] M<GOAL>(LinearMap.trace R P) (g ∘ₗ f ∘ₗ h) = (LinearMap.trace R N) (f ∘ₗ h ∘ₗ g)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup P<VAR>Module R P<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R P<VAR>Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : P →ₗ[R] M<GOAL>(LinearMap.trace R P) ((g ∘ₗ f) ∘ₗ h) = (LinearMap.trace R M) ((h ∘ₗ g) ∘ₗ f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] M<VAR>e : M ≃ₗ[R] N<GOAL>(LinearMap.trace R N) (e.conj f) = (LinearMap.trace R M) f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>h : LinearMap.IsProj p f<VAR>Module.Free R ↥p<VAR>Module.Finite R ↥p<VAR>Module.Free R ↥(LinearMap.ker f)<VAR>Module.Finite R ↥(LinearMap.ker f)<GOAL>(LinearMap.trace R M) f = ↑(FiniteDimensional.finrank R ↥p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : IsNilpotent f<GOAL>IsNilpotent ((LinearMap.trace R M) f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>IsReduced R<VAR>f g : Module.End R M<VAR>μ : R<VAR>h_comm : Commute f g<VAR>hg : IsNilpotent (g - (algebraMap R (Module.End R M)) μ)<GOAL>(LinearMap.trace R M) (f ∘ₗ g) = μ * (LinearMap.trace R M) f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>A : Type u_6<VAR>CommRing A<VAR>Algebra R A<GOAL>(LinearMap.trace A (TensorProduct R A M)) (LinearMap.baseChange A f) = (algebraMap R A) ((LinearMap.trace R M) f)
<VAR>K : Type u<VAR>Field K<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>(coevaluation K V) 1 = let bV := Basis.ofVectorSpace K V; ∑ i : ↑(Basis.ofVectorSpaceIndex K V), bV i ⊗ₜ[K] bV.coord i
<VAR>K : Type u<VAR>Field K<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V) = ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))
<VAR>K : Type u<VAR>Field K<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) = ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>T : Type u_7<VAR>U : Type u_8<VAR>CommRing R<VAR>Ring S<VAR>CommRing T<VAR>Ring U<VAR>Algebra R S<VAR>Algebra T U<VAR>φ : R →+* T<VAR>ψ : S →+* U<VAR>h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)<VAR>a : S<VAR>ha : IsIntegral R a<GOAL>IsIntegral T (ψ a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>Algebra.IsIntegral R B<GOAL>Algebra.IsIntegral R A
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A ≃ₐ[R] B<VAR>x : A<GOAL>IsIntegral R (f x) ↔ IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>x : B<VAR>hx : IsIntegral R x<GOAL>IsIntegral A x
<VAR>B : Type u_5<VAR>C : Type u_6<VAR>F : Type u_7<VAR>Ring B<VAR>Ring C<VAR>b : B<VAR>FunLike F B C<VAR>RingHomClass F B C<VAR>f : F<VAR>hb : IsIntegral ℤ b<GOAL>IsIntegral ℤ (f b)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>T : Subring R<VAR>hx : IsIntegral (↥T) x<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>x : A<VAR>h : IsIntegral R x<GOAL>IsIntegral R ((algebraMap A B) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>x : A<VAR>hAB : Function.Injective ⇑(algebraMap A B)<GOAL>IsIntegral R ((algebraMap A B) x) ↔ IsIntegral R x
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>r : B<GOAL>IsIntegral R r ↔ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set A<VAR>hfs : s.Finite<VAR>his : ∀ x ∈ s, IsIntegral R x<GOAL>(Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>IsNoetherianRing R<VAR>s : Finset A<VAR>hs : ∀ x ∈ s, IsIntegral R x<GOAL>IsNoetherian R ↥(Algebra.adjoin R ↑s)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<GOAL>IsNoetherian R B → ∀ (x : B), IsIntegral R x
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>S : Subalgebra R B<VAR>H : IsNoetherian R ↥(Subalgebra.toSubmodule S)<VAR>x : B<VAR>hx : x ∈ S<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_5<VAR>AddCommGroup M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>NoZeroSMulDivisors A M<VAR>N : Submodule R M<VAR>hN : N ≠ ⊥<VAR>hN' : N.FG<VAR>x : A<VAR>hx : ∀ n ∈ N, x • n ∈ N<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>h : f.Finite<GOAL>f.IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra.IsIntegral R A<VAR>h' : Algebra.FiniteType R A<GOAL>Module.Finite R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>h : f.IsIntegral<VAR>h' : f.FiniteType<GOAL>f.Finite
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>f.Finite ↔ f.IsIntegral ∧ f.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>r : A<GOAL>r ∈ integralClosure R A ↔ ∃ M, (Subalgebra.toSubmodule M).FG ∧ r ∈ M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : A<VAR>hx : IsIntegral R x<GOAL>Algebra.adjoin R {x} ≤ integralClosure R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S ≤ integralClosure R A ↔ Algebra.IsIntegral R ↥S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>S T : Subalgebra R A<GOAL>Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing S<VAR>Algebra R A<VAR>Algebra R S<VAR>f : A ≃ₐ[R] S<GOAL>Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing S<VAR>Algebra R A<VAR>Algebra R S<VAR>f : A →ₐ[R] S<VAR>x : ↥(integralClosure R A)<GOAL>↑(f.mapIntegralClosure x) = f ↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing S<VAR>Algebra R A<VAR>Algebra R S<VAR>f : A ≃ₐ[R] S<VAR>x : ↥(integralClosure R A)<GOAL>↑(f.mapIntegralClosure x) = f ↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : ↥(integralClosure R A)<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x y : B<VAR>r : R<VAR>hr : (algebraMap R B) r * y = 1<VAR>hx : IsIntegral R (x * y)<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : S<VAR>r : R<VAR>hr : f r * y = 1<VAR>hx : f.IsIntegralElem (x * y)<GOAL>f.IsIntegralElem x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>G : Set A<VAR>hG : ∀ x ∈ G, IsIntegral R x<VAR>x : A<GOAL>x ∈ Subring.closure G → IsIntegral R x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_5<VAR>CommRing S<VAR>f : R →+* S<VAR>G : Set S<VAR>hG : ∀ x ∈ G, f.IsIntegralElem x<VAR>x : S<GOAL>x ∈ Subring.closure G → f.IsIntegralElem x
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>h : IsIntegral R x<VAR>n : ℕ<GOAL>IsIntegral R (x ^ n)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>h : IsIntegral R x<VAR>n : ℕ<GOAL>IsIntegral R (n • x)
<VAR>R : Type u_1<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring B<VAR>Algebra R B<VAR>x : B<VAR>h : IsIntegral R x<VAR>n : ℤ<GOAL>IsIntegral R (n • x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Multiset A<VAR>h : ∀ x ∈ s, IsIntegral R x<GOAL>IsIntegral R s.prod
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Multiset A<VAR>h : ∀ x ∈ s, IsIntegral R x<GOAL>IsIntegral R s.sum
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>α : Type u_5<VAR>s : Finset α<VAR>f : α → A<VAR>h : ∀ x ∈ s, IsIntegral R (f x)<GOAL>IsIntegral R (∏ x ∈ s, f x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>α : Type u_5<VAR>s : Finset α<VAR>f : α → A<VAR>h : ∀ x ∈ s, IsIntegral R (f x)<GOAL>IsIntegral R (∑ x ∈ s, f x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>n : Type u_5<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n A<VAR>h : ∀ (i j : n), IsIntegral R (M i j)<GOAL>IsIntegral R M.det
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>IsIntegral R (x ^ n) ↔ IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>x : A<VAR>y : B<VAR>h : IsIntegral R y<GOAL>IsIntegral A (x ⊗ₜ[R] y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : R[X]<VAR>i : ℕ<VAR>hp : 1 ≤ p.natDegree<GOAL>(normalizeScaleRoots p).coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : R[X]<GOAL>p.leadingCoeff • normalizeScaleRoots p = p.scaleRoots p.leadingCoeff
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : R[X]<GOAL>(normalizeScaleRoots p).support ≤ p.support
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : R[X]<GOAL>(normalizeScaleRoots p).degree = p.degree
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>p : R[X]<VAR>h : 1 ≤ p.natDegree<VAR>f : R →+* S<VAR>x : S<GOAL>Polynomial.eval₂ f (f p.leadingCoeff * x) (normalizeScaleRoots p) = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : R[X]<VAR>h : p ≠ 0<GOAL>(normalizeScaleRoots p).Monic
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>h : Polynomial.eval₂ f x p = 0<GOAL>f.IsIntegralElem (f p.leadingCoeff * x)
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>p : R[X]<VAR>x : S<VAR>Algebra R S<VAR>h : (Polynomial.aeval x) p = 0<GOAL>IsIntegral R (p.leadingCoeff • x)
<VAR>A : Type u_1<VAR>R : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<GOAL>Function.Injective ⇑(algebraMap A B)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>x : A<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>Algebra R A<VAR>IsScalarTower R A B<GOAL>Algebra.IsIntegral R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>NoZeroSMulDivisors R B<GOAL>NoZeroSMulDivisors R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>x : B<VAR>hx : IsIntegral R x<GOAL>(algebraMap A B) (IsIntegralClosure.mk' A x hx) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>h : IsIntegral R 1 := ⋯<GOAL>IsIntegralClosure.mk' A 1 h = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>h : IsIntegral R 0 := ⋯<GOAL>IsIntegralClosure.mk' A 0 h = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>x y : B<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>IsIntegralClosure.mk' A (x + y) ⋯ = IsIntegralClosure.mk' A x hx + IsIntegralClosure.mk' A y hy
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>x y : B<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>IsIntegralClosure.mk' A (x * y) ⋯ = IsIntegralClosure.mk' A x hx * IsIntegralClosure.mk' A y hy
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>x : R<VAR>h : IsIntegral R ((algebraMap R B) x) := ⋯<GOAL>IsIntegralClosure.mk' A ((algebraMap R B) x) h = (algebraMap R A) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>S : Type u_4<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>isIntegral : Algebra.IsIntegral R S<VAR>x : S<GOAL>(algebraMap A B) ((IsIntegralClosure.lift R A B) x) = (algebraMap S B) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsIntegralClosure A R B<VAR>A' : Type u_4<VAR>CommRing A'<VAR>Algebra A' B<VAR>IsIntegralClosure A' R B<VAR>Algebra R A<VAR>Algebra R A'<VAR>IsScalarTower R A B<VAR>IsScalarTower R A' B<VAR>x : A<GOAL>(algebraMap A' B) ((IsIntegralClosure.equiv R A B A') x) = (algebraMap A B) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>Algebra R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>Algebra.IsIntegral R A<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>Algebra R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>Algebra.IsIntegral R A<VAR>Algebra.IsIntegral A B<GOAL>Algebra.IsIntegral R B
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : f.IsIntegral<VAR>hg : g.IsIntegral<GOAL>(g.comp f).IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_6<VAR>C : Type u_7<VAR>CommRing C<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra C B<VAR>IsScalarTower R A B<VAR>IsIntegralClosure C R B<VAR>Algebra.IsIntegral R A<GOAL>IsIntegralClosure C A B
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>f.IsIntegral
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>h : Function.Surjective ⇑(algebraMap R A)<GOAL>Algebra.IsIntegral R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>Algebra R B<VAR>Algebra R A<VAR>IsScalarTower R A B<VAR>H : Function.Injective ⇑(algebraMap A B)<VAR>x : A<VAR>h : IsIntegral R ((algebraMap A B) x)<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hg : Function.Injective ⇑g<VAR>hfg : (g.comp f).IsIntegral<GOAL>f.IsIntegral
<VAR>R : Type u_6<VAR>A : Type u_7<VAR>B : Type u_8<VAR>CommRing R<VAR>Field A<VAR>CommRing B<VAR>Nontrivial B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : A<VAR>h : IsIntegral R ((algebraMap A B) x)<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>x : T<VAR>h : (g.comp f).IsIntegralElem x<GOAL>g.IsIntegralElem x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>h : (g.comp f).IsIntegral<GOAL>g.IsIntegral
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>hf : f.IsIntegral<GOAL>(Ideal.quotientMap I f ⋯).IsIntegral
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<GOAL>(Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<GOAL>IsField R
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>hR : IsField R<GOAL>IsField S
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<GOAL>IsField R ↔ IsField S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>integralClosure (↑↑(integralClosure R A)) A = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>f : R[X]<VAR>hf : f.Monic<VAR>a : S<VAR>ha : a ∈ f.aroots S<GOAL>a ∈ integralClosure R S
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>CliffordAlgebra.involute ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι Q) m
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>CliffordAlgebra.involute.comp CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra Q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Function.Involutive ⇑CliffordAlgebra.involute