ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>PerfectField K<VAR>α : LieModule.Weight K (↥H) L<GOAL>↑(LieAlgebra.corootSpace ⇑α) = Submodule.span K {(LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)}
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>x : ↥H<VAR>α : ↥H → K<VAR>hαx : α x = 0<VAR>hx : x ∈ LieAlgebra.corootSpace α<GOAL>x = 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>Disjoint LieModule.Weight.ker (lieIdealSubalgebra K (↥H) (LieAlgebra.corootSpace ⇑α)).toSubmodule
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)) ≠ 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>α (LieAlgebra.IsKilling.coroot α) = 2
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>x : ↥H<GOAL>((LieModule.traceForm K (↥H) L) (LieAlgebra.IsKilling.coroot α)) x = 2 • (α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)))⁻¹ • α x
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>LieAlgebra.IsKilling.coroot α = 0 ↔ α.IsZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>Nontrivial L<GOAL>LieAlgebra.IsKilling.coroot 0 = 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>↑(LieAlgebra.corootSpace ⇑α) = Submodule.span K {LieAlgebra.IsKilling.coroot α}
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>LieAlgebra.corootSpace ⇑α = ⊥ ↔ α.IsZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>IsCompl LieModule.Weight.ker (Submodule.span K {LieAlgebra.IsKilling.coroot α})
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>x y : ↥H<VAR>hx : x ∈ LieModule.Weight.ker<VAR>hy : y ∈ Submodule.span K {LieAlgebra.IsKilling.coroot α}<GOAL>((LieModule.traceForm K (↥H) L) x) y = 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>(LieModule.traceForm K (↥H) L).orthogonal (Submodule.span K {LieAlgebra.IsKilling.coroot α}) = LieModule.Weight.ker
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α β : LieModule.Weight K (↥H) L<GOAL>LieAlgebra.IsKilling.coroot α = LieAlgebra.IsKilling.coroot β ↔ α = β
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ LieAlgebra.rootSpace H ⇑α ∧ f ∈ LieAlgebra.rootSpace H (-⇑α)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ LieAlgebra.rootSpace H ⇑α<VAR>hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)<GOAL>h = ↑(LieAlgebra.IsKilling.coroot α)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>FiniteDimensional.finrank K ↥↑(LieAlgebra.rootSpace H ⇑α) = 1
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<GOAL>⇑(-α) = -⇑α
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>h : α.IsZero<GOAL>(-α).IsZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<GOAL>(-α).IsZero ↔ α.IsZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<VAR>h : α.IsNonZero<GOAL>(-α).IsNonZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<GOAL>(-α).IsNonZero ↔ α.IsNonZero
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : LieModule.Weight K (↥H) L<GOAL>LieModule.Weight.toLinear K (↥H) L (-α) = -LieModule.Weight.toLinear K (↥H) L α
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>LieAlgebra.IsKilling K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>CharZero K<VAR>α : LieModule.Weight K (↥H) L<GOAL>LieAlgebra.IsKilling.coroot (-α) = -LieAlgebra.IsKilling.coroot α
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>LinearMap.ker f = ⊥
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>LinearMap.range f = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ LinearMap.ker f = ⊥
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ LinearMap.range f = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>Add R<GOAL>↑(AddMagmaCat.of R) = R
<VAR>R : Type u<VAR>Mul R<GOAL>↑(MagmaCat.of R) = R
<VAR>X Y : Type u_1<VAR>Mul X<VAR>Mul Y<VAR>e : X ≃* Y<GOAL>⇑↑e = ⇑e
<VAR>X Y : Type u_1<VAR>Add X<VAR>Add Y<VAR>e : X ≃+ Y<GOAL>⇑↑e = ⇑e
<VAR>X Y : Type u<VAR>Add X<VAR>Add Y<VAR>f : AddHom X Y<VAR>x : X<GOAL>(AddMagmaCat.ofHom f) x = f x
<VAR>X Y : Type u<VAR>Mul X<VAR>Mul Y<VAR>f : X →ₙ* Y<VAR>x : X<GOAL>(MagmaCat.ofHom f) x = f x
<VAR>R : Type u<VAR>AddSemigroup R<GOAL>↑(AddSemigrp.of R) = R
<VAR>R : Type u<VAR>Semigroup R<GOAL>↑(Semigrp.of R) = R
<VAR>X Y : Type u_1<VAR>Semigroup X<VAR>Semigroup Y<VAR>e : X ≃* Y<GOAL>⇑↑e = ⇑e
<VAR>X Y : Type u_1<VAR>AddSemigroup X<VAR>AddSemigroup Y<VAR>e : X ≃+ Y<GOAL>⇑↑e = ⇑e
<VAR>X Y : Type u<VAR>Semigroup X<VAR>Semigroup Y<VAR>f : X →ₙ* Y<VAR>x : X<GOAL>(Semigrp.ofHom f) x = f x
<VAR>X Y : Type u<VAR>AddSemigroup X<VAR>AddSemigroup Y<VAR>f : AddHom X Y<VAR>x : X<GOAL>(AddSemigrp.ofHom f) x = f x
<VAR>X Y : Type u<VAR>Mul X<VAR>Mul Y<VAR>e : X ≃* Y<GOAL>∀ (a : Y), e.toMagmaCatIso.inv a = e.symm.toFun a
<VAR>X Y : Type u<VAR>Add X<VAR>Add Y<VAR>e : X ≃+ Y<GOAL>∀ (a : X), e.toAddMagmaCatIso.hom a = e.toFun a
<VAR>X Y : Type u<VAR>Mul X<VAR>Mul Y<VAR>e : X ≃* Y<GOAL>∀ (a : X), e.toMagmaCatIso.hom a = e.toFun a
<VAR>X Y : Type u<VAR>Add X<VAR>Add Y<VAR>e : X ≃+ Y<GOAL>∀ (a : Y), e.toAddMagmaCatIso.inv a = e.symm.toFun a
<VAR>X Y : Type u<VAR>AddSemigroup X<VAR>AddSemigroup Y<VAR>e : X ≃+ Y<GOAL>∀ (a : Y), e.toAddSemigrpIso.inv a = e.symm.toFun a
<VAR>X Y : Type u<VAR>Semigroup X<VAR>Semigroup Y<VAR>e : X ≃* Y<GOAL>∀ (a : Y), e.toSemigrpIso.inv a = e.symm.toFun a
<VAR>X Y : Type u<VAR>AddSemigroup X<VAR>AddSemigroup Y<VAR>e : X ≃+ Y<GOAL>∀ (a : X), e.toAddSemigrpIso.hom a = e.toFun a
<VAR>X Y : Type u<VAR>Semigroup X<VAR>Semigroup Y<VAR>e : X ≃* Y<GOAL>∀ (a : X), e.toSemigrpIso.hom a = e.toFun a
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>(HopfAlgebraCat.of R X).str = inferInstance
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>(HopfAlgebraCat.of R X).instHopfAlgebra = inferInstance
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>↑(HopfAlgebraCat.of R X).toBundled = X
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>Coalgebra.counit = Coalgebra.counit
<VAR>R : Type u<VAR>CommRing R<VAR>V W : HopfAlgebraCat R<GOAL>Function.Injective HopfAlgebraCat.Hom.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : HopfAlgebraCat R<VAR>f g : X ⟶ Y<VAR>h : f.toBialgHom = g.toBialgHom<GOAL>f = g
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : HopfAlgebraCat R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).toBialgHom = g.toBialgHom.comp f.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>M : HopfAlgebraCat R<GOAL>(𝟙 M).toBialgHom = BialgHom.id R ↑M.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X : HopfAlgebraCat R<GOAL>(CategoryTheory.forget₂ (HopfAlgebraCat R) (BialgebraCat R)).obj X = BialgebraCat.of R ↑X.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : HopfAlgebraCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (HopfAlgebraCat R) (BialgebraCat R)).map f = BialgebraCat.ofHom f.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>HopfAlgebra R X<VAR>HopfAlgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.toHopfAlgebraCatIso.hom.toBialgHom = ↑e
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>HopfAlgebra R X<VAR>HopfAlgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.toHopfAlgebraCatIso.inv.toBialgHom = ↑e.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>Ring X<VAR>HopfAlgebra R X<GOAL>(BialgEquiv.refl R X).toHopfAlgebraCatIso = CategoryTheory.Iso.refl (HopfAlgebraCat.of R X)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Ring Y<VAR>HopfAlgebra R X<VAR>HopfAlgebra R Y<VAR>e : X ≃ₐc[R] Y<GOAL>e.symm.toHopfAlgebraCatIso = e.toHopfAlgebraCatIso.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : Type v<VAR>Ring X<VAR>Ring Y<VAR>Ring Z<VAR>HopfAlgebra R X<VAR>HopfAlgebra R Y<VAR>HopfAlgebra R Z<VAR>e : X ≃ₐc[R] Y<VAR>f : Y ≃ₐc[R] Z<GOAL>(e.trans f).toHopfAlgebraCatIso = e.toHopfAlgebraCatIso ≪≫ f.toHopfAlgebraCatIso
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : HopfAlgebraCat R<VAR>i : X ≅ Y<GOAL>↑i.toHopfAlgEquiv = i.hom.toBialgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X : HopfAlgebraCat R<GOAL>(CategoryTheory.Iso.refl X).toHopfAlgEquiv = BialgEquiv.refl R ↑X.toBundled
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : HopfAlgebraCat R<VAR>e : X ≅ Y<GOAL>e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : HopfAlgebraCat R<VAR>e : X ≅ Y<VAR>f : Y ≅ Z<GOAL>(e ≪≫ f).toHopfAlgEquiv = e.toHopfAlgEquiv.trans f.toHopfAlgEquiv
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>self : A →⋆ₙₐ[R] B<VAR>a : A<GOAL>self.toFun (star a) = star (self.toFun a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>F : Type u_6<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<GOAL>⇑f.toNonUnitalAlgHom = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f g : A →⋆ₙₐ[R] B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A → B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x<VAR>h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) = star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)<GOAL>⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →ₙₐ[R] B<VAR>h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)<GOAL>⇑{ toNonUnitalAlgHom := f, map_star' := h } = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x<VAR>h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) = star ({ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)<GOAL>{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<GOAL>⇑(NonUnitalStarAlgHom.id R A) = id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : B →⋆ₙₐ[R] C<VAR>g : A →⋆ₙₐ[R] B<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : B →⋆ₙₐ[R] C<VAR>g : A →⋆ₙₐ[R] B<VAR>a : A<GOAL>(f.comp g) a = f (g a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>NonUnitalNonAssocSemiring D<VAR>DistribMulAction R D<VAR>Star D<VAR>f : C →⋆ₙₐ[R] D<VAR>g : B →⋆ₙₐ[R] C<VAR>h : A →⋆ₙₐ[R] B<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<GOAL>(NonUnitalStarAlgHom.id R B).comp f = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>f : A →⋆ₙₐ[R] B<GOAL>f.comp (NonUnitalStarAlgHom.id R A) = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<GOAL>⇑1 = id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>a : A<GOAL>1 a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<VAR>a : A<GOAL>0 a = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>Star A<VAR>Star B<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →⋆ₙₐ[S] B<VAR>x : A<GOAL>(NonUnitalStarAlgHom.restrictScalars R f) x = f x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>Star A<VAR>Star B<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →⋆ₙₐ[S] B<GOAL>↑(NonUnitalStarAlgHom.restrictScalars R f) = ↑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>Star A<VAR>Star B<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →⋆ₙₐ[S] B<GOAL>⇑(NonUnitalStarAlgHom.restrictScalars R f) = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>Star A<VAR>Star B<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<GOAL>Function.Injective (NonUnitalStarAlgHom.restrictScalars R)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>self : A →⋆ₐ[R] B<VAR>x : A<GOAL>(↑↑self.toRingHom).toFun (star x) = star ((↑↑self.toRingHom).toFun x)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>F : Type u_7<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>StarAlgHomClass F R A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<GOAL>⇑f.toAlgHom = ⇑f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f g : A →⋆ₐ[R] B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f