ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → WithBot α<GOAL>∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithBot α<GOAL>⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithBot α<VAR>h : ∀ i ∈ s, f i ≠ ⊥<GOAL>⊥ < ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>DecidableEq α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithBot α<VAR>h : ∀ i ∈ s, f i ≠ ⊥<GOAL>⊥ < ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>h : f i = 0<GOAL>∏ j ∈ s, f j = 0
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>s : Finset ι<GOAL>(∏ i ∈ s, if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>s : Finset ι<VAR>f : ι → κ → M₀<GOAL>(Function.support fun x => ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, Function.support (f i)
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>Nontrivial M₀<VAR>NoZeroDivisors M₀<GOAL>∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>Nontrivial M₀<VAR>NoZeroDivisors M₀<GOAL>∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M₀ : Type u_4<VAR>CommMonoidWithZero M₀<VAR>Nontrivial M₀<VAR>NoZeroDivisors M₀<VAR>s : Finset ι<VAR>f : ι → κ → M₀<GOAL>(Function.support fun j => ∏ i ∈ s, f i j) = ⋂ i ∈ s, Function.support (f i)
<VAR>ι : Type u_1<VAR>M₀ : Type u_4<VAR>Fintype ι<VAR>CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>(∏ i : ι, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0
<VAR>ι : Type u_1<VAR>G₀ : Type u_3<VAR>CommGroupWithZero G₀<VAR>s : Finset ι<VAR>f : ι → G₀<VAR>h : ∏ i ∈ s, f i ≠ 0<GOAL>Units.mk0 (∏ i ∈ s, f i) h = ∏ i ∈ s.attach, Units.mk0 (f ↑i) ⋯
<VAR>R : Type u_2<VAR>OrderedSemiring R<GOAL>↑(Subsemiring.nonneg R) = Set.Ici 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ Finset.antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ Finset.antidiagonal n, f (p.1 + 1, p.2)
<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → N<GOAL>∑ p ∈ Finset.antidiagonal (n + 1), f p = f (0, n + 1) + ∑ p ∈ Finset.antidiagonal n, f (p.1 + 1, p.2)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ Finset.antidiagonal n, f p.swap = ∏ p ∈ Finset.antidiagonal n, f p
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∑ p ∈ Finset.antidiagonal n, f p.swap = ∑ p ∈ Finset.antidiagonal n, f p
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ Finset.antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p ∈ Finset.antidiagonal n, f (p.1, p.2 + 1)
<VAR>N : Type u_2<VAR>AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → N<GOAL>∑ p ∈ Finset.antidiagonal (n + 1), f p = f (n + 1, 0) + ∑ p ∈ Finset.antidiagonal n, f (p.1, p.2 + 1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → ℕ → M<GOAL>∑ p ∈ Finset.antidiagonal n, f p n = ∑ p ∈ Finset.antidiagonal n, f p (p.1 + p.2)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ<VAR>f : ℕ × ℕ → ℕ → M<GOAL>∏ p ∈ Finset.antidiagonal n, f p n = ∏ p ∈ Finset.antidiagonal n, f p (p.1 + p.2)
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>f : ℕ × ℕ → M<VAR>n : ℕ<GOAL>∑ ij ∈ Finset.antidiagonal n, f ij = ∑ k ∈ Finset.range n.succ, f (k, n - k)
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>f : ℕ × ℕ → M<VAR>n : ℕ<GOAL>∏ ij ∈ Finset.antidiagonal n, f ij = ∏ k ∈ Finset.range n.succ, f (k, n - k)
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∑ ij ∈ Finset.antidiagonal n, f ij.1 ij.2 = ∑ k ∈ Finset.range n.succ, f k (n - k)
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ ij ∈ Finset.antidiagonal n, f ij.1 ij.2 = ∏ k ∈ Finset.range n.succ, f k (n - k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>self : QuaternionAlgebra.Basis A c₁ c₂<GOAL>self.i * self.j = self.k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>self : QuaternionAlgebra.Basis A c₁ c₂<GOAL>self.i * self.i = c₁ • 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>self : QuaternionAlgebra.Basis A c₁ c₂<GOAL>self.j * self.j = c₂ • 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>self : QuaternionAlgebra.Basis A c₁ c₂<GOAL>self.j * self.i = -self.k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q₁ q₂ : QuaternionAlgebra.Basis A c₁ c₂<VAR>hi : q₁.i = q₂.i<VAR>hj : q₁.j = q₂.j<GOAL>q₁ = q₂
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(QuaternionAlgebra.Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(QuaternionAlgebra.Basis.self R).j = { re := 0, imI := 0, imJ := 1, imK := 0 }
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(QuaternionAlgebra.Basis.self R).k = { re := 0, imI := 0, imJ := 0, imK := 1 }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.i * q.k = c₁ • q.j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.k * q.i = -c₁ • q.j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.k * q.j = c₂ • q.i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.j * q.k = -c₂ • q.i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.k * q.k = -((c₁ * c₂) • 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.lift 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>q.lift 1 = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>q.lift (x + y) = q.lift x + q.lift y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>x y : ℍ[R,c₁,c₂]<GOAL>q.lift (x * y) = q.lift x * q.lift y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>r : R<VAR>x : ℍ[R,c₁,c₂]<GOAL>q.lift (r • x) = r • q.lift x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>a : ℍ[R,c₁,c₂]<GOAL>q.liftHom a = q.lift a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>(q.compHom F).i = F q.i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>(q.compHom F).j = F q.j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<VAR>F : A →ₐ[R] B<GOAL>(q.compHom F).k = F q.k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra.Basis A c₁ c₂<GOAL>QuaternionAlgebra.lift q = q.liftHom
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>F : ℍ[R,c₁,c₂] →ₐ[R] A<GOAL>QuaternionAlgebra.lift.symm F = (QuaternionAlgebra.Basis.self R).compHom F
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>c₁ c₂ : R<VAR>f g : ℍ[R,c₁,c₂] →ₐ[R] A<VAR>hi : f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i<VAR>hj : f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j<GOAL>f = g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>f g : ℍ[R] →ₐ[R] A<VAR>hi : f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i<VAR>hj : f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j<GOAL>f = g
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s : Multiset α<GOAL>p ∣ s.prod → ∃ a ∈ s, p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s : Multiset β<VAR>f : β → α<GOAL>p ∣ (Multiset.map f s).prod → ∃ a ∈ s, p ∣ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s : Finset β<VAR>f : β → α<GOAL>p ∣ s.prod f → ∃ i ∈ s, p ∣ f i
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Monoid M<VAR>Monoid N<VAR>x z : M × N<GOAL>x ~ᵤ z ↔ x.1 ~ᵤ z.1 ∧ x.2 ~ᵤ z.2
<VAR>M : Type u_5<VAR>CommMonoid M<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, f i ~ᵤ g i<GOAL>∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>s : Multiset α<GOAL>(∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>(a : α) → DecidablePred (Associated a)<VAR>s : Multiset α<VAR>n : α<VAR>h : ∀ a ∈ s, Prime a<VAR>div : ∀ a ∈ s, a ∣ n<VAR>uniq : ∀ (a : α), Multiset.countP (Associated a) s ≤ 1<GOAL>s.prod ∣ n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Unique αˣ<VAR>s : Finset α<VAR>n : α<VAR>h : ∀ a ∈ s, Prime a<VAR>div : ∀ a ∈ s, a ∣ n<GOAL>∏ p ∈ s, p ∣ n
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p : Multiset α<GOAL>(Multiset.map Associates.mk p).prod = Associates.mk p.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>p : Finset β<VAR>f : β → α<GOAL>∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p q : Multiset α<GOAL>Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p : Multiset (Associates α)<GOAL>p.prod = 1 ↔ ∀ a ∈ p, a = 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p q : Multiset (Associates α)<VAR>h : p ≤ q<GOAL>p.prod ≤ q.prod
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>s : Multiset (Associates α)<VAR>p : Associates α<VAR>hp : Prime p<GOAL>p ≤ s.prod → ∃ a ∈ s, p ≤ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Nontrivial α<VAR>s : Multiset α<VAR>h : ∀ x ∈ s, Prime x<GOAL>s.prod ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoidWithZero M<VAR>S : Finset α<VAR>p : M<VAR>pp : Prime p<VAR>g : α → M<GOAL>p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoidWithZero M<VAR>S : Finset α<VAR>p : M<VAR>pp : Prime p<VAR>g : α → M<VAR>hS : ∀ a ∈ S, ¬p ∣ g a<GOAL>¬p ∣ S.prod g
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoidWithZero M<VAR>f : α →₀ M<VAR>g : α → M → ℕ<VAR>p : ℕ<VAR>pp : Prime p<GOAL>p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoidWithZero M<VAR>f : α →₀ M<VAR>g : α → M → ℕ<VAR>p : ℕ<VAR>pp : Prime p<VAR>hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)<GOAL>¬p ∣ f.prod g
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>Even (∑ i ∈ s, f i) ↔ Even (Finset.filter (fun x => Odd (f x)) s).card
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>Odd (∑ i ∈ s, f i) ↔ Odd (Finset.filter (fun x => Odd (f x)) s).card
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SetLike S A<VAR>NonUnitalSubsemiringClass S A<VAR>hSR : SMulMemClass S R A<VAR>s : S<GOAL>⇑(NonUnitalSubalgebraClass.subtype s) = Subtype.val
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>s : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S T : NonUnitalSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑S.toNonUnitalSubsemiring = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<GOAL>Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S U : NonUnitalSubalgebra R A<GOAL>S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toSubmodule ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑S.toSubmodule = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<GOAL>Function.Injective NonUnitalSubalgebra.toSubmodule
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S U : NonUnitalSubalgebra R A<GOAL>S.toSubmodule = U.toSubmodule ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>s : Set A<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalNonAssocRing A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toNonUnitalSubring ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalNonAssocRing A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑S.toNonUnitalSubring = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalNonAssocRing A<VAR>Module R A<GOAL>Function.Injective NonUnitalSubalgebra.toNonUnitalSubring
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>NonUnitalNonAssocRing A<VAR>Module R A<VAR>S U : NonUnitalSubalgebra R A<GOAL>S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>↑0 = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : ↥S<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : NonUnitalSubalgebra R A<VAR>x y : ↥S<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>Semiring R'<VAR>SMul R' R<VAR>Module R' A<VAR>IsScalarTower R' R A<VAR>r : R'<VAR>x : ↥S<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<VAR>x : ↥S<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : NonUnitalSubalgebra R A<GOAL>NonUnitalSubringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S₁ S₂ : NonUnitalSubalgebra R A<VAR>f : F<GOAL>S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.map f S₂
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (NonUnitalSubalgebra.map f)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>NonUnitalSubalgebra.map (NonUnitalAlgHom.id R A) S = S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R A<VAR>Module R B<VAR>Module R C<VAR>S : NonUnitalSubalgebra R A<VAR>g : B →ₙₐ[R] C<VAR>f : A →ₙₐ[R] B<GOAL>NonUnitalSubalgebra.map g (NonUnitalSubalgebra.map f S) = NonUnitalSubalgebra.map (g.comp f) S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>f : F<VAR>y : B<GOAL>y ∈ NonUnitalSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>f : F<GOAL>(NonUnitalSubalgebra.map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>f : F<GOAL>(NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>f : F<GOAL>↑(NonUnitalSubalgebra.map f S) = ⇑f '' ↑S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>f : F<VAR>U : NonUnitalSubalgebra R B<GOAL>NonUnitalSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalSubalgebra.comap f U
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<GOAL>GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R B<VAR>f : F<VAR>x : A<GOAL>x ∈ NonUnitalSubalgebra.comap f S ↔ f x ∈ S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R A<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R B<VAR>f : F<GOAL>↑(NonUnitalSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>p : Submodule R A<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<VAR>x : A<GOAL>x ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>p : Submodule R A<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<GOAL>↑(p.toNonUnitalSubalgebra h_mul) = ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>p : Submodule R A<VAR>hmul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<GOAL>p.toNonUnitalSubalgebra hmul = { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>p : Submodule R A<VAR>h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p<GOAL>(p.toNonUnitalSubalgebra h_mul).toSubmodule = p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>S : NonUnitalSubalgebra R A<GOAL>S.toSubmodule.toNonUnitalSubalgebra ⋯ = S
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>φ : F<VAR>y : B<GOAL>y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, φ x = y
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>φ : F<VAR>x : A<GOAL>φ x ∈ NonUnitalAlgHom.range φ
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>φ : F<GOAL>↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R C<VAR>f : A →ₙₐ[R] B<VAR>g : B →ₙₐ[R] C<GOAL>NonUnitalAlgHom.range (g.comp f) = NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>NonUnitalNonAssocSemiring C<VAR>Module R C<VAR>f : A →ₙₐ[R] B<VAR>g : B →ₙₐ[R] C<GOAL>NonUnitalAlgHom.range (g.comp f) ≤ NonUnitalAlgHom.range g
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>(NonUnitalSubalgebraClass.subtype S).comp (NonUnitalAlgHom.codRestrict f S hf) = NonUnitalAlgHomClass.toNonUnitalAlgHom f
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<VAR>x : A<GOAL>↑((NonUnitalAlgHom.codRestrict f S hf) x) = f x
<VAR>F : Type v'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>NonUnitalNonAssocSemiring B<VAR>Module R B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>S : NonUnitalSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>Function.Injective ⇑(NonUnitalAlgHom.codRestrict f S hf) ↔ Function.Injective ⇑f