ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>x : L<GOAL>φ.nilRank ≤ (LinearMap.charpoly (φ x)).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>x : L<GOAL>φ.IsNilRegular x ↔ (LinearMap.charpoly (φ x)).coeff φ.nilRank ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>x : L<GOAL>φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>x : L<GOAL>φ.IsNilRegular x ↔ (LinearMap.charpoly (φ x)).natTrailingDegree = φ.nilRank
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>IsDomain R<VAR>h : ↑(FiniteDimensional.finrank R M) ≤ Cardinal.mk R<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>IsDomain R<VAR>Infinite R<GOAL>∃ x, φ.IsNilRegular x
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>GradedMonoid.GMonoid A<VAR>(i : ιB) → AddMonoid (M i)<VAR>self : DirectSum.GdistribMulAction A M<VAR>i : ιA<VAR>j : ιB<VAR>a : A i<VAR>b c : M j<GOAL>GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>GradedMonoid.GMonoid A<VAR>(i : ιB) → AddMonoid (M i)<VAR>self : DirectSum.GdistribMulAction A M<VAR>i : ιA<VAR>j : ιB<VAR>a : A i<GOAL>GradedMonoid.GSMul.smul a 0 = 0
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddMonoid (A i)<VAR>(i : ιB) → AddMonoid (M i)<VAR>GradedMonoid.GMonoid A<VAR>self : DirectSum.Gmodule A M<VAR>i : ιA<VAR>j : ιB<VAR>a a' : A i<VAR>b : M j<GOAL>GradedMonoid.GSMul.smul (a + a') b = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddMonoid (A i)<VAR>(i : ιB) → AddMonoid (M i)<VAR>GradedMonoid.GMonoid A<VAR>self : DirectSum.Gmodule A M<VAR>i : ιA<VAR>j : ιB<VAR>b : M j<GOAL>GradedMonoid.GSMul.smul 0 b = 0
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>GradedMonoid.GMonoid A<VAR>DirectSum.Gmodule A M<VAR>i : ιA<VAR>j : ιB<VAR>a : A i<VAR>b : M j<GOAL>((DirectSum.gsmulHom A M) a) b = GradedMonoid.GSMul.smul a b
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>DecidableEq ιA<VAR>DecidableEq ιB<VAR>GradedMonoid.GMonoid A<VAR>DirectSum.Gmodule A M<VAR>x : ⨁ (i : ιA), A i<VAR>y : ⨁ (i : ιB), M i<GOAL>x • y = ((DirectSum.Gmodule.smulAddMonoidHom A M) x) y
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>DecidableEq ιA<VAR>DecidableEq ιB<VAR>GradedMonoid.GMonoid A<VAR>DirectSum.Gmodule A M<VAR>i : ιA<VAR>j : ιB<VAR>x : A i<VAR>y : M j<GOAL>((DirectSum.Gmodule.smulAddMonoidHom A M) ((DirectSum.of A i) x)) ((DirectSum.of M j) y) = (DirectSum.of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>DecidableEq ιA<VAR>DecidableEq ιB<VAR>GradedMonoid.GMonoid A<VAR>DirectSum.Gmodule A M<VAR>i : ιA<VAR>j : ιB<VAR>x : A i<VAR>y : M j<GOAL>(DirectSum.of A i) x • (DirectSum.of M j) y = (DirectSum.of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>DecidableEq ιA<VAR>DecidableEq ιB<VAR>GradedMonoid.GMonoid A<VAR>DirectSum.Gmodule A M<VAR>x : ⨁ (i : ιB), M i<GOAL>1 • x = x
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>AddMonoid ιA<VAR>VAdd ιA ιB<VAR>(i : ιA) → AddCommMonoid (A i)<VAR>(i : ιB) → AddCommMonoid (M i)<VAR>DecidableEq ιA<VAR>DecidableEq ιB<VAR>DirectSum.GSemiring A<VAR>DirectSum.Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<GOAL>(a * b) • c = a • b • c
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<GOAL>MvPolynomial.aeval f = MvPolynomial.bind₁ f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<GOAL>MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<GOAL>MvPolynomial.eval₂Hom f MvPolynomial.X = MvPolynomial.bind₂ f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.aeval id = MvPolynomial.join₁
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial (MvPolynomial σ R) R<GOAL>(MvPolynomial.eval₂Hom MvPolynomial.C id) φ = MvPolynomial.join₁ φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X = MvPolynomial.join₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>i : σ<GOAL>(MvPolynomial.bind₁ f) (MvPolynomial.X i) = f i
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<VAR>i : σ<GOAL>(MvPolynomial.bind₂ f) (MvPolynomial.X i) = MvPolynomial.X i
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.bind₁ MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>x : R<GOAL>(MvPolynomial.bind₁ f) (MvPolynomial.C x) = MvPolynomial.C x
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<VAR>r : R<GOAL>(MvPolynomial.bind₂ f) (MvPolynomial.C r) = f r
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.bind₂ MvPolynomial.C = RingHom.id (MvPolynomial σ R)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<GOAL>(MvPolynomial.bind₂ f).comp MvPolynomial.C = f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.join₂ ((MvPolynomial.map f) φ) = (MvPolynomial.bind₂ f) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<GOAL>MvPolynomial.join₂.comp (MvPolynomial.map f) = MvPolynomial.bind₂ f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval id) ((MvPolynomial.rename f) p) = (MvPolynomial.aeval f) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.join₁ ((MvPolynomial.rename f) φ) = (MvPolynomial.bind₁ f) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.bind₁ id = MvPolynomial.join₁
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.bind₂ (RingHom.id (MvPolynomial σ R)) = MvPolynomial.join₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → MvPolynomial υ R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.bind₁ g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.bind₁ g) (f i)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → MvPolynomial υ R<GOAL>(MvPolynomial.bind₁ g).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.bind₁ g) (f i)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* MvPolynomial σ T<GOAL>(MvPolynomial.bind₂ g).comp (MvPolynomial.bind₂ f) = MvPolynomial.bind₂ ((MvPolynomial.bind₂ g).comp f)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* MvPolynomial σ T<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.bind₂ g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ ((MvPolynomial.bind₂ g).comp f)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → υ<GOAL>(MvPolynomial.rename g).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.rename g) (f i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → υ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.rename g) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename g) (f i)) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* T<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.map g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ ((MvPolynomial.map g).comp f)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : τ → MvPolynomial υ R<VAR>g : σ → τ<GOAL>(MvPolynomial.bind₁ f).comp (MvPolynomial.rename g) = MvPolynomial.bind₁ (f ∘ g)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>υ : Type u_6<VAR>f : τ → MvPolynomial υ R<VAR>g : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.bind₁ f) ((MvPolynomial.rename g) φ) = (MvPolynomial.bind₁ (f ∘ g)) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : S →+* MvPolynomial σ T<VAR>g : R →+* S<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.bind₂ f) ((MvPolynomial.map g) φ) = (MvPolynomial.bind₂ (f.comp g)) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<GOAL>(MvPolynomial.map f).comp MvPolynomial.C = MvPolynomial.C.comp f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : MvPolynomial τ R →+* S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>f ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.eval₂Hom (f.comp MvPolynomial.C) fun i => f (g i)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.map f) ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.map f) (g i)) ((MvPolynomial.map f) φ)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : σ → S<GOAL>(MvPolynomial.eval₂Hom f g).comp MvPolynomial.C = f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : τ → S<VAR>h : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₁ h) φ) = (MvPolynomial.eval₂Hom f fun i => (MvPolynomial.eval₂Hom f g) (h i)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>f : τ → S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.aeval fun i => (MvPolynomial.aeval f) (g i)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>f : τ → S<VAR>g : σ → MvPolynomial τ R<GOAL>(MvPolynomial.aeval f).comp (MvPolynomial.bind₁ g) = MvPolynomial.aeval fun i => (MvPolynomial.aeval f) (g i)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : S →+* T<VAR>g : σ → T<VAR>h : R →+* MvPolynomial σ S<GOAL>(MvPolynomial.eval₂Hom f g).comp (MvPolynomial.bind₂ h) = MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>f : S →+* T<VAR>g : σ → T<VAR>h : R →+* MvPolynomial σ S<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₂ h) φ) = (MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring T<VAR>Algebra S T<VAR>f : σ → T<VAR>g : R →+* MvPolynomial σ S<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.aeval f) ((MvPolynomial.bind₂ g) φ) = (MvPolynomial.eval₂Hom ((↑(MvPolynomial.aeval f)).comp g) f) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.bind₁ f) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * ∏ i ∈ d.support, f i ^ d i
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) r) = f r * (MvPolynomial.monomial d) 1
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* MvPolynomial σ S<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) 1) = (MvPolynomial.monomial d) 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>DecidableEq τ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>((MvPolynomial.bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<VAR>j : τ<VAR>h : j ∈ ((MvPolynomial.bind₁ f) φ).vars<GOAL>∃ i ∈ φ.vars, j ∈ (f i).vars
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>↑(Ideal.torsionOf R M x) = ⇑(LinearMap.toSpanSingleton R M x) ⁻¹' {0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Ideal.torsionOf R M 0 = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>a : R<GOAL>a ∈ Ideal.torsionOf R M x ↔ a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>Ideal.torsionOf R M m = ⊤ ↔ m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>m : M<GOAL>Ideal.torsionOf R M m = ⊥ ↔ m ≠ 0
<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : CompleteLattice.Independent fun i => Submodule.span R {v i}<VAR>h_ne_zero : ∀ (i : ι), Ideal.torsionOf R M (v i) = ⊥<GOAL>LinearIndependent R v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>a : R<GOAL>(Ideal.quotTorsionOfEquivSpanSingleton R M x) (Submodule.Quotient.mk a) = a • ⟨x, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>↑(Submodule.torsionBy R M a) = ⇑(DistribMulAction.toLinearMap R M a) ⁻¹' {0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>↑(Submodule.torsionBySet R M s) = ⋂ y ∈ s, ⇑(DistribMulAction.toLinearMap R M y) ⁻¹' {0}
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<GOAL>↑(Submodule.torsion'AddSubMonoid M S) = {x | ∃ a, a • x = 0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommMonoid S<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<GOAL>↑(Submodule.torsion' R M S) = {x | ∃ a, a • x = 0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.IsTorsionBySet R M ↑(Module.annihilator R M)
<VAR>R : Type u_2<VAR>M : Type u_1<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>IsSMulRegular M r ↔ Submodule.torsionBy R M r = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<VAR>x : ↥(Submodule.torsionBy R M a)<GOAL>a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<VAR>x : ↥(Submodule.torsionBy R M a)<GOAL>a • ↑x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<VAR>x : M<GOAL>x ∈ Submodule.torsionBy R M a ↔ a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<VAR>x : M<GOAL>x ∈ Submodule.torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Submodule.torsionBySet R M {a} = Submodule.torsionBy R M a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set R<VAR>st : s ⊆ t<GOAL>Submodule.torsionBySet R M t ≤ Submodule.torsionBySet R M s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Submodule.torsionBySet R M s = Submodule.torsionBySet R M ↑(Ideal.span s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Submodule.torsionBySet R M ↑(Submodule.span R {a}) = Submodule.torsionBy R M a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a b : R<VAR>dvd : a ∣ b<GOAL>Submodule.torsionBy R M a ≤ Submodule.torsionBy R M b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.torsionBy R M 1 = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.torsionBySet R M Set.univ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Module.IsTorsionBySet R M {a} ↔ Module.IsTorsionBy R M a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R M s ↔ Submodule.torsionBySet R M s = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Module.IsTorsionBy R M a ↔ Submodule.torsionBy R M a = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R M s ↔ Module.IsTorsionBySet R M ↑(Ideal.span s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Module.IsTorsionBySet R M ↑(Submodule.span R {a}) ↔ Module.IsTorsionBy R M a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R M s ↔ s ⊆ ↑(LinearMap.ker (LinearMap.lsmul R M))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Module.IsTorsionBy R M a ↔ a ∈ LinearMap.ker (LinearMap.lsmul R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R (↥(Submodule.torsionBySet R M s)) s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Module.IsTorsionBy R (↥(Submodule.torsionBy R M a)) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : R<GOAL>Submodule.torsionBy R (↥(Submodule.torsionBy R M a)) a = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<GOAL>Submodule.torsionBySet R (↥(Submodule.torsionBySet R M s)) s = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>GaloisConnection Submodule.annihilator fun I => Submodule.torsionBySet R M ↑(OrderDual.ofDual I)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<GOAL>⨆ i ∈ S, Submodule.torsionBySet R M ↑(p i) = Submodule.torsionBySet R M ↑(⨅ i ∈ S, p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<GOAL>S.SupIndep fun i => Submodule.torsionBySet R M ↑(p i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (∏ i ∈ S, q i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_3<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<GOAL>S.SupIndep fun i => Submodule.torsionBy R M (q i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>DecidableEq ι<VAR>S : Finset ι<VAR>p : ι → Ideal R<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)<GOAL>DirectSum.IsInternal fun i => Submodule.torsionBySet R M ↑(p ↑i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>DecidableEq ι<VAR>S : Finset ι<VAR>q : ι → R<VAR>hq : (↑S).Pairwise (IsCoprime on q)<VAR>hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)<GOAL>DirectSum.IsInternal fun i => Submodule.torsionBy R M (q ↑i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>hM : Module.IsTorsionBySet R M ↑I<VAR>b : R<VAR>x : M<GOAL>(Ideal.Quotient.mk I) b • x = b • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>hM : Module.IsTorsionBy R M r<VAR>b : R<VAR>x : M<GOAL>(Ideal.Quotient.mk (Ideal.span {r})) b • x = b • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>Module.IsTorsionBy R (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<VAR>h : Module.IsTorsionBy R M r<GOAL>Module.IsTorsionBy R (M ⧸ N) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>s : Set R<GOAL>Module.IsTorsionBySet R (M ⧸ N) s ↔ ∀ (x : M), ∀ r ∈ s, r • x ∈ N