ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>BinomialRing R<VAR>NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<GOAL>(n + k).choose k • Ring.choose (r + ↑k) (n + k) = Ring.choose (r + ↑k) k * Ring.choose r n
<VAR>R : Type u_1<VAR>Ring R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>(descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ Finset.antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
<VAR>R : Type u_1<VAR>Ring R<VAR>BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>Ring.choose (r + s) k = ∑ ij ∈ Finset.antidiagonal k, Ring.choose r ij.1 * Ring.choose s ij.2
<VAR>R : Type u<VAR>Semiring R<VAR>self : IsPrincipalIdealRing R<VAR>S : Ideal R<GOAL>Submodule.IsPrincipal S
<VAR>R : Type u<VAR>Semiring R<GOAL>IsPrincipalIdealRing R ↔ ∀ (S : Ideal R), Submodule.IsPrincipal S
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>0 ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>a b : α<GOAL>a ∈ I → b ∈ I → a + b ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>a : α<VAR>b : α<GOAL>b ∈ I → a * b ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I J : Ideal α<VAR>h : ∀ (x : α), x ∈ I ↔ x ∈ J<GOAL>I = J
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>f : ι → α<GOAL>(∀ c ∈ t, f c ∈ I) → ∑ i ∈ t, f i ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>x y : α<VAR>hx : x ∈ I<VAR>h : y * x = 1<GOAL>I = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>x : α<VAR>hx : x ∈ I<VAR>h : IsUnit x<GOAL>I = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>I = ⊤ ↔ 1 ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>I ≠ ⊤ ↔ 1 ∉ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>x y : α<VAR>hy : IsUnit y<GOAL>y * x ∈ I ↔ x ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<GOAL>Submodule.span α s = Ideal.span s
<VAR>α : Type u<VAR>Semiring α<GOAL>Ideal.span ∅ = ⊥
<VAR>α : Type u<VAR>Semiring α<GOAL>Ideal.span Set.univ = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>s t : Set α<GOAL>Ideal.span (s ∪ t) = Ideal.span s ⊔ Ideal.span t
<VAR>α : Type u<VAR>Semiring α<VAR>ι : Sort u_1<VAR>s : ι → Set α<GOAL>Ideal.span (⋃ i, s i) = ⨆ i, Ideal.span (s i)
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ Ideal.span s ↔ ∀ (p : Ideal α), s ⊆ ↑p → x ∈ p
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<GOAL>s ⊆ ↑(Ideal.span s)
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<VAR>I : Ideal α<GOAL>Ideal.span s ≤ I ↔ s ⊆ ↑I
<VAR>α : Type u<VAR>Semiring α<VAR>s t : Set α<GOAL>s ⊆ t → Ideal.span s ≤ Ideal.span t
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>Ideal.span ↑I = I
<VAR>α : Type u<VAR>Semiring α<GOAL>Ideal.span {1} = ⊤
<VAR>α : Type u<VAR>Semiring α<GOAL>CompleteLattice.IsCompactElement ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<VAR>x y : α<GOAL>x ∈ Ideal.span (insert y s) ↔ ∃ a, ∃ z ∈ Ideal.span s, x = a * y + z
<VAR>α : Type u<VAR>Semiring α<VAR>x y : α<GOAL>x ∈ Ideal.span {y} ↔ ∃ a, a * y = x
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>x : α<GOAL>Ideal.span {x} ≤ I ↔ x ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>Ideal.span {a * x} = Ideal.span {x}
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>s : Set α<GOAL>Ideal.span (insert x s) = Ideal.span {x} ⊔ Ideal.span s
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<GOAL>Ideal.span s = ⊥ ↔ ∀ x ∈ s, x = 0
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<GOAL>Ideal.span {x} = ⊥ ↔ x = 0
<VAR>α : Type u_1<VAR>CommSemiring α<VAR>x : α<VAR>hx : ¬IsUnit x<GOAL>Ideal.span {x} ≠ ⊤
<VAR>α : Type u<VAR>Semiring α<GOAL>Ideal.span 0 = ⊥
<VAR>α : Type u<VAR>Semiring α<GOAL>Ideal.span 1 = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set α<GOAL>Ideal.span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ Ideal.span ↑s' = ⊤
<VAR>S : Type u_1<VAR>CommSemiring S<VAR>x y : S<VAR>I : Ideal S<GOAL>x ∈ Ideal.span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>self : I.IsPrime<VAR>x y : α<GOAL>x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>self : I.IsPrime<GOAL>I ≠ ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<GOAL>I ≠ ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<VAR>x y : α<GOAL>x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<VAR>x y : α<VAR>h : x * y = 0<GOAL>x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<VAR>r : α<VAR>n : ℕ<VAR>H : r ^ n ∈ I<GOAL>r ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>h : I ≠ ⊤<GOAL>0 ≠ 1
<VAR>α : Type u<VAR>Semiring α<VAR>IsDomain α<GOAL>⊥.IsPrime
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>self : I.IsMaximal<GOAL>IsCoatom I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>I.IsMaximal ↔ IsCoatom I
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>h : I.IsMaximal<GOAL>I ≠ ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<GOAL>I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
<VAR>α : Type u<VAR>Semiring α<VAR>I J : Ideal α<VAR>hI : I.IsMaximal<VAR>hJ : J ≠ ⊤<VAR>IJ : I ≤ J<GOAL>I = J
<VAR>α : Type u<VAR>Semiring α<VAR>M M' : Ideal α<VAR>hM : M.IsMaximal<VAR>hM' : M'.IsMaximal<VAR>hne : M ≠ M'<GOAL>M ⊔ M' = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I ≠ ⊤<GOAL>∃ M, M.IsMaximal ∧ I ≤ M
<VAR>α : Type u<VAR>Semiring α<VAR>Nontrivial α<GOAL>∃ M, M.IsMaximal
<VAR>α : Type u<VAR>Semiring α<VAR>P : Ideal α<VAR>hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal<VAR>J : Ideal α<VAR>hPJ : P < J<GOAL>J = ⊤
<VAR>α : Type u<VAR>Semiring α<VAR>x y : α<GOAL>Ideal.span {x, y} = Ideal.span {y, x}
<VAR>α : Type u<VAR>Semiring α<VAR>x y z : α<GOAL>z ∈ Ideal.span {x, y} ↔ ∃ a b, a * x + b * y = z
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>z : R<GOAL>Ideal.span {x + y * z, y} = Ideal.span {x, y}
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>z : R<GOAL>Ideal.span {x, y + x * z} = Ideal.span {x, y}
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>hI : I.IsMaximal<VAR>x : α<VAR>hx : x ∉ I<GOAL>∃ y, ∃ i ∈ I, y * x + i = 1
<VAR>R : Type u<VAR>Semiring R<VAR>S T : Ideal R<VAR>x : R<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u<VAR>Semiring R<VAR>S T : Ideal R<VAR>x : R<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Sort u_1<VAR>S : ι → Ideal R<VAR>i : ι<VAR>x : R<GOAL>x ∈ S i → x ∈ iSup S
<VAR>R : Type u<VAR>Semiring R<VAR>S : Set (Ideal R)<VAR>s : Ideal R<VAR>hs : s ∈ S<VAR>x : R<GOAL>x ∈ s → x ∈ sSup S
<VAR>R : Type u<VAR>Semiring R<VAR>s : Set (Ideal R)<VAR>x : R<GOAL>x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I
<VAR>R : Type u<VAR>Semiring R<VAR>I J : Ideal R<VAR>x : R<GOAL>x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Sort u_1<VAR>I : ι → Ideal R<VAR>x : R<GOAL>x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
<VAR>R : Type u<VAR>Semiring R<VAR>x : R<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>ι : Type v<VAR>x : ι → α<GOAL>x ∈ I.pi ι ↔ ∀ (i : ι), x i ∈ I
<VAR>α : Type u<VAR>Semiring α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<GOAL>(sInf s).IsPrime
<VAR>α : Type u<VAR>CommSemiring α<VAR>I : Ideal α<VAR>x y : α<VAR>hy : IsUnit y<GOAL>x * y ∈ I ↔ x ∈ I
<VAR>α : Type u<VAR>CommSemiring α<VAR>x y : α<GOAL>x ∈ Ideal.span {y} ↔ y ∣ x
<VAR>α : Type u<VAR>CommSemiring α<VAR>x : α<GOAL>x ∈ Ideal.span {x}
<VAR>α : Type u<VAR>CommSemiring α<VAR>x y : α<GOAL>Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x
<VAR>α : Type u<VAR>CommRing α<VAR>IsDomain α<VAR>x y : α<GOAL>Ideal.span {x} = Ideal.span {y} ↔ Associated x y
<VAR>α : Type u<VAR>CommSemiring α<VAR>a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>Ideal.span {x * a} = Ideal.span {x}
<VAR>α : Type u<VAR>CommSemiring α<VAR>x : α<GOAL>Ideal.span {x} = ⊤ ↔ IsUnit x
<VAR>α : Type u<VAR>CommSemiring α<VAR>p : α<VAR>hp : p ≠ 0<GOAL>(Ideal.span {p}).IsPrime ↔ Prime p
<VAR>α : Type u<VAR>CommSemiring α<VAR>I : Ideal α<VAR>H : I.IsMaximal<GOAL>I.IsPrime
<VAR>α : Type u<VAR>CommSemiring α<VAR>IsDomain α<VAR>x y : α<GOAL>Ideal.span {x} < Ideal.span {y} ↔ DvdNotUnit y x
<VAR>α : Type u<VAR>CommSemiring α<VAR>IsDomain α<VAR>b₁ b₂ : α<VAR>h₁ : b₁ ≠ 0<VAR>h₂ : ¬IsUnit b₂<GOAL>Ideal.span {b₁ * b₂} < Ideal.span {b₁}
<VAR>α : Type u<VAR>a : α<VAR>b : α<VAR>CommSemiring α<VAR>I : Ideal α<VAR>h : a ∈ I<GOAL>a * b ∈ I
<VAR>α : Type u<VAR>a : α<VAR>CommSemiring α<VAR>I : Ideal α<VAR>ha : a ∈ I<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>a ^ n ∈ I
<VAR>α : Type u<VAR>a : α<VAR>CommSemiring α<VAR>I : Ideal α<VAR>m n : ℕ<VAR>ha : a ^ m ∈ I<VAR>h : m ≤ n<GOAL>a ^ n ∈ I
<VAR>α : Type u<VAR>a b : α<VAR>CommSemiring α<VAR>I : Ideal α<VAR>m n k : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<VAR>hk : m + n ≤ k + 1<GOAL>(a + b) ^ k ∈ I
<VAR>α : Type u<VAR>a b : α<VAR>CommSemiring α<VAR>I : Ideal α<VAR>m n : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<GOAL>(a + b) ^ (m + n - 1) ∈ I
<VAR>α : Type u<VAR>CommSemiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<VAR>x y : α<GOAL>x * y ∈ I ↔ x ∈ I ∨ y ∈ I
<VAR>α : Type u<VAR>CommSemiring α<VAR>I : Ideal α<VAR>hI : I.IsPrime<VAR>r : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>r ^ n ∈ I ↔ r ∈ I
<VAR>α : Type u<VAR>CommSemiring α<VAR>DecidableEq α<VAR>s : Multiset α<VAR>n : ℕ<GOAL>s.sum ^ (Multiset.card s * n + 1) ∈ Ideal.span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
<VAR>α : Type u<VAR>CommSemiring α<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ Ideal.span ((fun i => f i ^ (n + 1)) '' ↑s)
<VAR>α : Type u<VAR>CommSemiring α<VAR>s : Set α<VAR>hs : Ideal.span s = ⊤<VAR>n : ℕ<GOAL>Ideal.span ((fun x => x ^ n) '' s) = ⊤
<VAR>α : Type u<VAR>CommSemiring α<VAR>I : Ideal α<VAR>S : Submonoid α<VAR>disjoint : Disjoint ↑I ↑S<VAR>maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S<GOAL>I.IsPrime
<VAR>α : Type u<VAR>Ring α<VAR>I : Ideal α<VAR>a : α<GOAL>-a ∈ I ↔ a ∈ I
<VAR>α : Type u<VAR>Ring α<VAR>I : Ideal α<VAR>a b : α<GOAL>b ∈ I → (a + b ∈ I ↔ a ∈ I)
<VAR>α : Type u<VAR>Ring α<VAR>I : Ideal α<VAR>a b : α<GOAL>a ∈ I → (a + b ∈ I ↔ b ∈ I)
<VAR>α : Type u<VAR>Ring α<VAR>I : Ideal α<VAR>a b : α<GOAL>a ∈ I → b ∈ I → a - b ∈ I
<VAR>α : Type u<VAR>Ring α<VAR>s : Set α<VAR>x y : α<GOAL>x ∈ Ideal.span (insert y s) ↔ ∃ a, x + a * y ∈ Ideal.span s
<VAR>α : Type u<VAR>Ring α<VAR>x : α<GOAL>Ideal.span {-x} = Ideal.span {x}
<VAR>K : Type u<VAR>DivisionSemiring K<VAR>I : Ideal K<GOAL>I = ⊥ ∨ I = ⊤
<VAR>K : Type u<VAR>DivisionSemiring K<VAR>I : Ideal K<VAR>h : I.IsPrime<GOAL>I = ⊥
<VAR>K : Type u<VAR>DivisionSemiring K<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>a b c d : R<VAR>h1 : a - b ∈ I<VAR>h2 : c - d ∈ I<GOAL>a * c - b * d ∈ I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>hf : ¬IsField R<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>IsField R ↔ IsSimpleOrder (Ideal R)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>M : Ideal R<VAR>max : M.IsMaximal<VAR>not_field : ¬IsField R<GOAL>M ≠ ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<VAR>M : Ideal R<VAR>hm : M.IsMaximal<VAR>non_field : ¬IsField R<GOAL>⊥ < M
<VAR>α : Type u<VAR>a : α<VAR>Monoid α<GOAL>a ∈ nonunits α ↔ ¬IsUnit a
<VAR>α : Type u<VAR>a b : α<VAR>CommMonoid α<GOAL>b ∈ nonunits α → a * b ∈ nonunits α
<VAR>α : Type u<VAR>a b : α<VAR>CommMonoid α<GOAL>a ∈ nonunits α → a * b ∈ nonunits α
<VAR>α : Type u<VAR>Semiring α<GOAL>0 ∈ nonunits α ↔ 0 ≠ 1
<VAR>α : Type u<VAR>Monoid α<GOAL>1 ∉ nonunits α
<VAR>α : Type u<VAR>Semiring α<VAR>I : Ideal α<VAR>h : I ≠ ⊤<GOAL>↑I ⊆ nonunits α
<VAR>α : Type u<VAR>a : α<VAR>CommSemiring α<VAR>h : a ∈ nonunits α<GOAL>∃ I, I.IsMaximal ∧ a ∈ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>a : A<VAR>x : M<GOAL>(LinearMap.baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>⇑(LinearMap.baseChange A f) = ⇑(LinearMap.lTensor A f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f g : M →ₗ[R] N<GOAL>LinearMap.baseChange A (f + g) = LinearMap.baseChange A f + LinearMap.baseChange A g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>LinearMap.baseChange A 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>r : R<VAR>f : M →ₗ[R] N<GOAL>LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.baseChange A LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<GOAL>LinearMap.baseChange A (g ∘ₗ f) = LinearMap.baseChange A g ∘ₗ LinearMap.baseChange A f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.baseChange A 1 = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : Module.End R M<GOAL>LinearMap.baseChange A (f * g) = LinearMap.baseChange A f * LinearMap.baseChange A g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>(LinearMap.baseChangeHom R A M N) f = LinearMap.baseChange A f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : Module.End R M<GOAL>∀ (a_1 : A ⊗[R] M), ((Module.End.baseChangeHom R A M) a) a_1 = (TensorProduct.liftAux (↑R ({ toFun := fun h => h ∘ₗ a, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ TensorProduct.AlgebraTensorModule.mk R A A M))) a_1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.End R M<VAR>n : ℕ<GOAL>LinearMap.baseChange A (f ^ n) = LinearMap.baseChange A f ^ n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f g : M →ₗ[R] N<GOAL>LinearMap.baseChange A (f - g) = LinearMap.baseChange A f - LinearMap.baseChange A g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>LinearMap.baseChange A (-f) = -LinearMap.baseChange A f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>l : M →ₗ[R] N<VAR>x : A<VAR>y : M<GOAL>(LinearMap.liftBaseChange A l) (x ⊗ₜ[R] y) = x • l y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>l : M →ₗ[R] N<VAR>y : M<GOAL>(LinearMap.liftBaseChange A l) (1 ⊗ₜ[R] y) = l y
<VAR>R : Type u_4<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>l : A ⊗[R] M →ₗ[A] N<VAR>x : M<GOAL>((LinearMap.liftBaseChangeEquiv A).symm l) x = l (1 ⊗ₜ[R] x)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>P : Type u_1<VAR>AddCommMonoid P<VAR>Module A P<VAR>Module R P<VAR>IsScalarTower R A P<VAR>l : M →ₗ[R] N<VAR>l' : N →ₗ[A] P<GOAL>l' ∘ₗ LinearMap.liftBaseChange A l = LinearMap.liftBaseChange A (↑R l' ∘ₗ l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>l : M →ₗ[R] N<GOAL>LinearMap.range (LinearMap.liftBaseChange A l) = Submodule.span A ↑(LinearMap.range l)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>AddCommMonoidWithOne A<VAR>Module R A<VAR>AddCommMonoidWithOne B<VAR>Module R B<GOAL>1 = 1 ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>AddCommMonoidWithOne A<VAR>Module R A<VAR>AddCommMonoidWithOne B<VAR>Module R B<VAR>n : ℕ<GOAL>↑n = ↑n ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>AddCommMonoidWithOne A<VAR>Module R A<VAR>AddCommMonoidWithOne B<VAR>Module R B<VAR>n : ℕ<GOAL>↑n = 1 ⊗ₜ[R] ↑n
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>a₁ a₂ : A<VAR>b₁ b₂ : B<GOAL>(Algebra.TensorProduct.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>a₁ a₂ : A<VAR>b₁ b₂ : B<GOAL>a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>a₁ a₂ a₃ : A<VAR>b₁ b₂ b₃ : B<VAR>ha : SemiconjBy a₁ a₂ a₃<VAR>hb : SemiconjBy b₁ b₂ b₃<GOAL>SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>a₁ a₂ : A<VAR>b₁ b₂ : B<VAR>ha : Commute a₁ a₂<VAR>hb : Commute b₁ b₂<GOAL>Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>x : A ⊗[R] B<GOAL>(Algebra.TensorProduct.mul (1 ⊗ₜ[R] 1)) x = x
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonAssocSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>x : A ⊗[R] B<GOAL>(Algebra.TensorProduct.mul x) (1 ⊗ₜ[R] 1) = x
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>NonUnitalSemiring B<VAR>Module R B<VAR>SMulCommClass R B B<VAR>IsScalarTower R B B<VAR>x y z : A ⊗[R] B<GOAL>(Algebra.TensorProduct.mul ((Algebra.TensorProduct.mul x) y)) z = (Algebra.TensorProduct.mul x) ((Algebra.TensorProduct.mul y) z)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>a : A<VAR>b : B<VAR>k : ℕ<GOAL>a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>a : A<GOAL>Algebra.TensorProduct.includeLeftRingHom a = a ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CommSemiring S<VAR>Algebra S A<VAR>SMulCommClass R S A<VAR>r : S<GOAL>(algebraMap S (A ⊗[R] B)) r = (algebraMap S A) r ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>r : R<GOAL>(algebraMap R (A ⊗[R] B)) r = 1 ⊗ₜ[R] (algebraMap R B) r
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CommSemiring S<VAR>Algebra S A<VAR>SMulCommClass R S A<VAR>a : A<GOAL>Algebra.TensorProduct.includeLeft a = a ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>b : B<GOAL>Algebra.TensorProduct.includeRight b = 1 ⊗ₜ[R] b
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<GOAL>Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap R A) = Algebra.TensorProduct.includeRight.comp (algebraMap R B)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>CommSemiring S<VAR>Algebra S A<VAR>Algebra R S<VAR>Algebra S C<VAR>IsScalarTower R S A<VAR>IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp Algebra.TensorProduct.includeLeft = g.comp Algebra.TensorProduct.includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight = (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight<GOAL>f = g
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>CommSemiring S<VAR>Algebra S A<VAR>Algebra R S<VAR>Algebra S C<VAR>IsScalarTower R S A<VAR>IsScalarTower R S C<VAR>g h : A ⊗[R] B →ₐ[S] C<VAR>H : ∀ (a : A) (b : B), g (a ⊗ₜ[R] b) = h (a ⊗ₜ[R] b)<GOAL>g = h
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>AddCommGroupWithOne A<VAR>Module R A<VAR>AddCommGroupWithOne B<VAR>Module R B<VAR>z : ℤ<GOAL>↑z = ↑z ⊗ₜ[R] 1
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Ring B<VAR>Algebra R B<VAR>z : ℤ<GOAL>↑z = 1 ⊗ₜ[R] ↑z
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>Semiring A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra S C<VAR>f : A ⊗[R] B →ₗ[S] C<VAR>h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)<VAR>h_one : f (1 ⊗ₜ[R] 1) = 1<VAR>x : A ⊗[R] B<GOAL>(Algebra.TensorProduct.algHomOfLinearMapTensorProduct f h_mul h_one) x = f x