ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>e'' : M₂ ≃ₛₗ[σ₂₃] M₃<VAR>l : M →ₛₗ[σ₁₂] M₂<GOAL>LinearMap.ker ((↑e'').comp l) = LinearMap.ker l
<VAR>R : Type u<VAR>M : Type v<VAR>VAdd R M<VAR>s : ULift.{u_1, u} R<VAR>x : M<GOAL>s +ᵥ x = s.down +ᵥ x
<VAR>R : Type u<VAR>M : Type v<VAR>SMul R M<VAR>s : ULift.{u_1, u} R<VAR>x : M<GOAL>s • x = s.down • x
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : ULift.{w, v} M<GOAL>ULift.moduleEquiv self = self.down
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>down : M<GOAL>ULift.moduleEquiv.symm down = { down := down }
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>self : Module R M<VAR>x : M<GOAL>0 • x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>self : Module R M<VAR>r s : R<VAR>x : M<GOAL>(r + s) • x = r • x + s • x
<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>n : ℕ<GOAL>↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r s : R<VAR>x : M<GOAL>(r + s) • x = r • x + s • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a b : R<VAR>h : a + b = 1<VAR>x : M<GOAL>a • x + b • x = x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>2 • x = x + x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>2 • x = 2 • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Invertible 2<VAR>x : M<GOAL>⅟2 • x + ⅟2 • x = x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : R<GOAL>∀ (x_1 : M), ((Module.toAddMonoidEnd R M) x) x_1 = x • x_1
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>x : M<GOAL>((smulAddHom R M) r) x = r • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>zero_eq_one : 0 = 1<GOAL>x = 0
<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>R : Type u_9<VAR>Ring R<VAR>Module R M<VAR>r : R<VAR>m : M<GOAL>r • m + (1 - r) • m = m
<VAR>M : Type u_5<VAR>AddCommGroup M<VAR>z : ℤ<GOAL>↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>a b : R<VAR>h : a + b = 1<GOAL>a • x + b • y = b • (y - x) + x
<VAR>R : Type u_9<VAR>Semiring R<VAR>M : Type u_10<VAR>AddCommMonoid M<VAR>P Q : Module R M<VAR>w : ∀ (r : R) (m : M), r • m = r • m<GOAL>P = Q
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>x : M<GOAL>-r • x = -(r • x)
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>x : M<GOAL>-r • -x = r • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>u : Rˣ<VAR>x : M<GOAL>-u • x = -(u • x)
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<GOAL>-1 • x = -x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r s : R<VAR>y : M<GOAL>(r - s) • y = r • y - s • y
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>Subsingleton R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Subsingleton M
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>Nontrivial M<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Nontrivial R
<VAR>R : Type u_2<VAR>S : Type u_4<VAR>Semiring R<VAR>NonAssocSemiring S<VAR>Module R S<VAR>IsScalarTower R S S<VAR>x : R<GOAL>RingHom.smulOneHom x = x • 1
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : M<GOAL>↑n • b = n • b
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>b : M<GOAL>OfNat.ofNat n • b = OfNat.ofNat n • b
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>b : M<GOAL>n • b = ↑n • b
<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>h : Module ℕ M<VAR>n : ℕ<VAR>x : M<GOAL>SMul.smul n x = n • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℤ<VAR>b : M<GOAL>↑n • b = n • b
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℤ<VAR>b : M<GOAL>n • b = ↑n • b
<VAR>M : Type u_5<VAR>AddCommGroup M<VAR>h : Module ℤ M<VAR>n : ℤ<VAR>x : M<GOAL>SMul.smul n x = n • x
<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_10<VAR>S : Type u_11<VAR>Ring R<VAR>Ring S<VAR>Module R M<VAR>Module S M₂<VAR>x : ℤ<VAR>a : M<GOAL>f (↑x • a) = ↑x • f a
<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_10<VAR>S : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>Module R M<VAR>Module S M₂<VAR>x : ℕ<VAR>a : M<GOAL>f (↑x • a) = ↑x • f a
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Zero R<VAR>Zero M<VAR>SMul R M<VAR>self : NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<GOAL>c • x = 0 → c = 0 ∨ x = 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Zero R<VAR>Zero M<VAR>SMul R M<GOAL>NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>N : Type u_11<VAR>Zero R<VAR>Zero M<VAR>Zero N<VAR>SMul R M<VAR>SMul R N<VAR>NoZeroSMulDivisors R N<VAR>f : M → N<VAR>hf : Function.Injective f<VAR>h0 : f 0 = 0<VAR>hs : ∀ (c : R) (x : M), f (c • x) = c • f x<GOAL>NoZeroSMulDivisors R M
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMul R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<VAR>hc : c ≠ 0<VAR>hx : x ≠ 0<GOAL>c • x ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<GOAL>c • x = 0 ↔ c = 0 ∨ x = 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<GOAL>c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<VAR>hx : x ≠ 0<GOAL>c • x = 0 ↔ c = 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<VAR>hc : c ≠ 0<GOAL>c • x = 0 ↔ x = 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<VAR>hx : x ≠ 0<GOAL>c • x ≠ 0 ↔ c ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Zero R<VAR>Zero M<VAR>SMulWithZero R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<VAR>hc : c ≠ 0<GOAL>c • x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<GOAL>NoZeroSMulDivisors ℕ M
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommMonoid M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<GOAL>2 • v = 0 ↔ v = 0
<VAR>R : Type u_2<VAR>Semiring R<VAR>M : Type u_9<VAR>AddCommMonoidWithOne M<VAR>CharZero M<VAR>Module R M<GOAL>CharZero R
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>hc : c ≠ 0<GOAL>Function.Injective fun x => c • x
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>hc : c ≠ 0<VAR>x y : M<GOAL>c • x = c • y ↔ x = y
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<GOAL>v = -v ↔ v = 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<GOAL>-v = v ↔ v = 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<GOAL>v ≠ -v ↔ v ≠ 0
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Semiring R<VAR>CharZero R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<GOAL>-v ≠ v ↔ v ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>Function.Injective fun c => c • x
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>CharZero R<GOAL>NoZeroSMulDivisors ℤ M
<VAR>R : Type u_2<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>NoZeroSMulDivisors ℤ M<GOAL>CharZero R
<VAR>R : Type u_9<VAR>NonAssocSemiring R<VAR>m : ℕ<GOAL>m • 1 = ↑m
<VAR>R : Type u_9<VAR>NonAssocRing R<VAR>m : ℤ<GOAL>m • 1 = ↑m
<VAR>R : Type u<VAR>E : Type v<VAR>AddCommGroup E<VAR>Ring R<VAR>Module R E<VAR>Nontrivial E<VAR>NoZeroSMulDivisors R E<GOAL>Cardinal.lift.{v, u} (Cardinal.mk R) ≤ Cardinal.lift.{u, v} (Cardinal.mk E)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin n) R<VAR>h : ∀ (x : Fin n → R), (MvPolynomial.eval x) p = 0<GOAL>p = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>σ : Type u_2<VAR>p q : MvPolynomial σ R<VAR>h : ∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q<GOAL>p = q
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>σ : Type u_2<VAR>p q : MvPolynomial σ R<GOAL>p = q ↔ ∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>x : τ → R<VAR>i : σ<GOAL>MvPolynomial.comap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>x : σ → R<GOAL>MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) x = x
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<GOAL>MvPolynomial.comap (AlgHom.id R (MvPolynomial σ R)) = id
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<VAR>x : υ → R<GOAL>MvPolynomial.comap (g.comp f) x = MvPolynomial.comap f (MvPolynomial.comap g x)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<GOAL>MvPolynomial.comap (g.comp f) = MvPolynomial.comap f ∘ MvPolynomial.comap g
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R<VAR>hf : ∀ (φ : MvPolynomial σ R), f φ = φ<VAR>x : σ → R<GOAL>MvPolynomial.comap f x = x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>x : τ → R<GOAL>MvPolynomial.comap (MvPolynomial.rename f) x = x ∘ f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R<GOAL>⇑(MvPolynomial.comapEquiv f) = MvPolynomial.comap ↑f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R<GOAL>⇑(MvPolynomial.comapEquiv f).symm = MvPolynomial.comap ↑f.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>IsLocalizedModule.IsInteger f 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>x y : M'<VAR>hx : IsLocalizedModule.IsInteger f x<VAR>hy : IsLocalizedModule.IsInteger f y<GOAL>IsLocalizedModule.IsInteger f (x + y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>a : R<VAR>x : M'<VAR>hx : IsLocalizedModule.IsInteger f x<GOAL>IsLocalizedModule.IsInteger f (a • x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>x : M'<GOAL>∃ a, IsLocalizedModule.IsInteger f (↑a • x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>g : ι → M'<GOAL>∃ b, ∀ i ∈ s, IsLocalizedModule.IsInteger f (↑b • g i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>ι : Type u_4<VAR>Finite ι<VAR>g : ι → M'<GOAL>∃ b, ∀ (i : ι), IsLocalizedModule.IsInteger f (↑b • g i)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>s : Finset M'<GOAL>∃ b, ∀ a ∈ s, IsLocalizedModule.IsInteger f (↑b • a)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>g : ι → M'<VAR>i : { x // x ∈ s }<GOAL>f (IsLocalizedModule.integerMultiple S f s g i) = IsLocalizedModule.commonDenom S f s g • g ↑i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>DecidableEq M<VAR>s : Finset M'<GOAL>⇑f '' ↑(IsLocalizedModule.finsetIntegerMultiple S f s) = IsLocalizedModule.commonDenomOfFinset S f s • ↑s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>hx : f x ∈ Submodule.span R ↑s<GOAL>∃ m, m • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S f s)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra A B<VAR>b : B<GOAL>(MvPolynomial.ACounit A B) (MvPolynomial.X b) = b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra A B<VAR>a : A<GOAL>(MvPolynomial.ACounit A B) (MvPolynomial.C a) = (algebraMap A B) a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra A B<GOAL>Function.Surjective ⇑(MvPolynomial.ACounit A B)
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Function.Surjective ⇑(MvPolynomial.counit R)
<VAR>A : Type u_1<VAR>CommSemiring A<GOAL>Function.Surjective ⇑(MvPolynomial.counitNat A)
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℤ<GOAL>(MvPolynomial.counit R) (MvPolynomial.C n) = ↑n
<VAR>A : Type u_1<VAR>CommSemiring A<VAR>n : ℕ<GOAL>(MvPolynomial.counitNat A) (MvPolynomial.C n) = ↑n
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<GOAL>(MvPolynomial.counit R) (MvPolynomial.X r) = r
<VAR>A : Type u_1<VAR>CommSemiring A<VAR>a : A<GOAL>(MvPolynomial.counitNat A) (MvPolynomial.X a) = a
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>Nonempty σ<VAR>Nontrivial R<GOAL>#(MvPolynomial σ R) = max (max (Cardinal.lift.{u, v} #R) (Cardinal.lift.{v, u} #σ)) ℵ₀
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>IsEmpty σ<GOAL>#(MvPolynomial σ R) = Cardinal.lift.{u, v} #R
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<GOAL>#(MvPolynomial σ R) ≤ max (max (Cardinal.lift.{u, v} #R) (Cardinal.lift.{v, u} #σ)) ℵ₀
<VAR>σ R : Type u<VAR>CommSemiring R<VAR>Nonempty σ<VAR>Nontrivial R<GOAL>#(MvPolynomial σ R) = max (max #R #σ) ℵ₀
<VAR>σ R : Type u<VAR>CommSemiring R<GOAL>#(MvPolynomial σ R) ≤ max (max #R #σ) ℵ₀
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submodule R M<GOAL>↑(-S) = -↑S
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submodule R M<GOAL>(-S).toAddSubmonoid = -S.toAddSubmonoid
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>g : M<VAR>S : Submodule R M<GOAL>g ∈ -S ↔ -g ∈ S
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<GOAL>-S ≤ -T ↔ S ≤ T
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<GOAL>-S ≤ T ↔ S ≤ -T
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R (-s) = -Submodule.span R s
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<GOAL>-(S ⊓ T) = -S ⊓ -T
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<GOAL>-(S ⊔ T) = -S ⊔ -T
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>-⊥ = ⊥
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>-⊤ = ⊤
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Sort u_4<VAR>S : ι → Submodule R M<GOAL>-⨅ i, S i = ⨅ i, -S i
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Sort u_4<VAR>S : ι → Submodule R M<GOAL>-⨆ i, S i = ⨆ i, -S i
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>-p = p
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p + q = p ⊔ q
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>0 = ⊥
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<VAR>S : Submodule R M<GOAL>↑(a • S) = a • ↑S
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<VAR>S : Submodule R M<GOAL>(a • S).toAddSubmonoid = a • S.toAddSubmonoid
<VAR>α : Type u_1<VAR>Monoid α<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>DistribMulAction α M<VAR>Module R M<VAR>SMulCommClass α R M<VAR>a : α<VAR>S : Submodule R M<GOAL>(a • S).toAddSubgroup = a • S.toAddSubgroup
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>m : M<VAR>a : α<VAR>S : Submodule R M<GOAL>m ∈ S → a • m ∈ a • S
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<GOAL>a • ⊥ = ⊥
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<VAR>S T : Submodule R M<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<VAR>s : Set M<GOAL>a • Submodule.span R s = Submodule.span R (a • s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Monoid α<VAR>DistribMulAction α M<VAR>SMulCommClass α R M<VAR>a : α<VAR>s : Set M<GOAL>Submodule.span R (a • s) = a • Submodule.span R s
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_4<VAR>Semiring α<VAR>Module α R<VAR>Module α M<VAR>SMulCommClass α R M<VAR>IsScalarTower α R M<VAR>a : α<VAR>S : Submodule R M<GOAL>a • S ≤ S
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N : Submodule R M<VAR>x : M<GOAL>x ∈ s • N ↔ x ∈ sInf {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N : Submodule R M<VAR>r : S<VAR>m : M<VAR>mem1 : r ∈ s<VAR>mem2 : m ∈ N<GOAL>r • m ∈ s • N
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N p : Submodule R M<VAR>closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p<GOAL>s • N ≤ p
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N p : Submodule R M<GOAL>s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N p : Submodule R M<VAR>closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p<VAR>le : p ≤ s • N<GOAL>s • N = p
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>p q : Submodule R M<VAR>le : p ≤ q<GOAL>s • p ≤ s • q
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>N : Submodule R M<VAR>s t : Set S<VAR>le : s ≤ t<GOAL>s • N ≤ t • N
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s t : Set S<VAR>p q : Submodule R M<VAR>le_set : s ≤ t<VAR>le_submodule : p ≤ q<GOAL>s • p ≤ t • q
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : Set S<VAR>N : Submodule R M<GOAL>s • N = ⨆ a ∈ s, a • N
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : Set S<VAR>t : Set M<GOAL>s • Submodule.span R t = Submodule.span R (s • t)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>SMulCommClass S R M<VAR>s : Set S<VAR>t : Set M<GOAL>Submodule.span R (s • t) = s • Submodule.span R t
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>s : Set S<VAR>N : Submodule R M<VAR>motive : (x : M) → x ∈ s • N → Prop<VAR>x : M<VAR>hx : x ∈ s • N<VAR>smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯<VAR>smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯<VAR>add : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯<VAR>zero : motive 0 ⋯<GOAL>motive x hx
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>sR : Set R<VAR>N : Submodule R M<VAR>SMulCommClass R R ↥N<GOAL>sR • N = Submodule.map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>sR : Set R<VAR>N : Submodule R M<VAR>x : M<VAR>SMulCommClass R R ↥N<GOAL>x ∈ sR • N ↔ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>S : Type u_4<VAR>Monoid S<VAR>AddCommMonoid M<VAR>Module R M<VAR>DistribMulAction S M<VAR>N : Submodule R M<GOAL>∅ • N = ⊥