ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>Polynomial.nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing S<VAR>IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>CommRing R<VAR>Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>↑((IsPrimitiveRoot.autToPow R hμ) f) = ↑⋯.choose
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing S<VAR>IsDomain S<VAR>μ : S<VAR>n : ℕ+<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>CommRing R<VAR>Algebra R S<VAR>f : S ≃ₐ[R] S<GOAL>μ ^ (↑((IsPrimitiveRoot.autToPow R hμ) f)).val = f μ
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective BialgEquiv.toEquiv
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e₁ e₂ : A ≃ₐc[R] B<GOAL>e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective BialgEquiv.toBialgHom
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e₁ e₂ : A ≃ₐc[R] B<GOAL>↑e₁ = ↑e₂ ↔ e₁ = e₂
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A → B<VAR>h : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₀ : ∀ (m : R) (x : A), { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x<VAR>h₁ : Coalgebra.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = Coalgebra.counit<VAR>h₂ : TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }<VAR>h₃ : B → A<VAR>h₄ : Function.LeftInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun<VAR>h₅ : Function.RightInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun<VAR>h₆ : ∀ (x y : A), { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun (x * y) = { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun x * { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun y<GOAL>⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅, map_mul' := h₆ } = f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>⇑↑e = ⇑e
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A ≃ₐc[R] B<GOAL>f.toCoalgEquiv = ↑f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A ≃ₐc[R] B<GOAL>f.toBialgHom = ↑f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A ≃ₐc[R] B<GOAL>f.toAlgEquiv = ↑f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>↑e = ↑↑e
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>↑↑e = ↑e
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₐc[R] B<VAR>h : ∀ (x : A), e x = e' x<GOAL>e = e'
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₐc[R] B<GOAL>e = e' ↔ ∀ (x : A), e x = e' x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<VAR>x x' : A<GOAL>x = x' → e x = e x'
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e e' : A ≃ₐc[R] B<VAR>h : e = e'<VAR>x : A<GOAL>e x = e' x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>a : A<GOAL>(BialgEquiv.refl R A) a = a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>∀ (a : A), (BialgEquiv.refl R A).invFun a = a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>↑(BialgEquiv.refl R A) = CoalgEquiv.refl R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>↑(BialgEquiv.refl R A) = BialgHom.id R A
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>↑e.symm = (↑e).symm
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>e.invFun = ⇑e.symm
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e : A ≃ₐc[R] B<GOAL>e.toEquiv.symm = ↑e.symm
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₐc[R] B<VAR>e₂₃ : B ≃ₐc[R] C<GOAL>∀ (a : C), (e₁₂.trans e₂₃).invFun a = (↑↑e₁₂).symm ((↑↑e₂₃).symm a)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₐc[R] B<VAR>e₂₃ : B ≃ₐc[R] C<GOAL>∀ (a : A), (e₁₂.trans e₂₃) a = ↑e₂₃ (↑e₁₂ a)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₐc[R] B<VAR>e₂₃ : B ≃ₐc[R] C<GOAL>↑(e₁₂.trans e₂₃) = (↑e₁₂).trans ↑e₂₃
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₐc[R] B<VAR>e₂₃ : B ≃ₐc[R] C<GOAL>↑(e₁₂.trans e₂₃) = (↑e₂₃).comp ↑e₁₂
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type u₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Semiring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>e₁₂ : A ≃ₐc[R] B<VAR>e₂₃ : B ≃ₐc[R] C<GOAL>(↑e₁₂).trans ↑e₂₃ = ↑(e₁₂.trans e₂₃)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>self : DiscreteValuationRing R<GOAL>LocalRing.maximalIdeal R ≠ ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>LocalRing.maximalIdeal R ≠ ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>¬IsField R
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : LocalRing.maximalIdeal R = Ideal.span {ϖ}<GOAL>Irreducible ϖ
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>ϖ : R<GOAL>Irreducible ϖ ↔ LocalRing.maximalIdeal R = Ideal.span {ϖ}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>ϖ : R<VAR>h : Irreducible ϖ<GOAL>LocalRing.maximalIdeal R = Ideal.span {ϖ}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>∃ ϖ, Irreducible ϖ
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>∃ ϖ, Prime ϖ
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>DiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : Irreducible b<GOAL>Associated a b
<VAR>R : Type u_1<VAR>CommRing R<VAR>hR : DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<GOAL>Associated p q
<VAR>R : Type u_1<VAR>CommRing R<VAR>hR : DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R<VAR>IsDomain R<GOAL>UniqueFactorizationMonoid R
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>UniqueFactorizationMonoid R<VAR>h₁ : ∃ p, Irreducible p<VAR>h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q<GOAL>DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>UniqueFactorizationMonoid R<VAR>h₁ : ∃ p, Irreducible p<VAR>h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>UniqueFactorizationMonoid R<VAR>h₁ : ∃ p, Irreducible p<VAR>h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q<GOAL>DiscreteValuationRing R
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>hR : DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R<GOAL>DiscreteValuationRing R
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<GOAL>∃ n, Associated x (ϖ ^ n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<GOAL>∃ n u, x = ↑u * ϖ ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<GOAL>∃ n, s = Ideal.span {ϖ ^ n}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * p ^ m = ↑v * q ^ n<GOAL>m = n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * ϖ ^ m = ↑v * ϖ ^ n<GOAL>u = v
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>r : R<VAR>u : Rˣ<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>n : ℕ<VAR>hr : r = ↑u * ϖ ^ n<GOAL>(DiscreteValuationRing.addVal R) r = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>u : Rˣ<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>n : ℕ<GOAL>(DiscreteValuationRing.addVal R) (↑u * ϖ ^ n) = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>(DiscreteValuationRing.addVal R) 0 = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>(DiscreteValuationRing.addVal R) 1 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<GOAL>(DiscreteValuationRing.addVal R) ϖ = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a b : R<GOAL>(DiscreteValuationRing.addVal R) (a * b) = (DiscreteValuationRing.addVal R) a + (DiscreteValuationRing.addVal R) b
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a : R<VAR>n : ℕ<GOAL>(DiscreteValuationRing.addVal R) (a ^ n) = n • (DiscreteValuationRing.addVal R) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>ϖ : R<VAR>h : Irreducible ϖ<VAR>n : ℕ<GOAL>(DiscreteValuationRing.addVal R) (ϖ ^ n) = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a : R<GOAL>(DiscreteValuationRing.addVal R) a = ⊤ ↔ a = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a b : R<GOAL>(DiscreteValuationRing.addVal R) a ≤ (DiscreteValuationRing.addVal R) b ↔ a ∣ b
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<VAR>a b : R<GOAL>min ((DiscreteValuationRing.addVal R) a) ((DiscreteValuationRing.addVal R) b) ≤ (DiscreteValuationRing.addVal R) (a + b)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>f₁ f₂ : A →ₐ[R] B<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<VAR>x : A<GOAL>↑((diffToIdealOfQuotientCompEq I f₁ f₂ e) x) = f₁ x - f₂ x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>f : A →ₐ[R] B<VAR>e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)<VAR>x : A<GOAL>↑((derivationToSquareZeroOfLift I hI f e) x) = f x - (algebraMap A B) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>f : Derivation R A ↥I<VAR>x : A<GOAL>(liftOfDerivationToSquareZero I hI f) x = ↑(f x) + (algebraMap A B) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>Algebra A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>f : { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }<VAR>c : A<GOAL>↑(((derivationToSquareZeroEquivLift I hI).symm f) c) = ↑f c - (algebraMap A B) c
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>↑((derivationToSquareZeroEquivLift I hI) d) x = ↑(d x) + (algebraMap A B) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>F : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>Semiring B<VAR>Bialgebra R B<VAR>FunLike F A B<VAR>BialgHomClass F R A B<VAR>f : F<GOAL>(Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>F : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>Semiring B<VAR>Bialgebra R B<VAR>FunLike F A B<VAR>BialgHomClass F R A B<VAR>f : F<GOAL>(Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>F : Type u_6<VAR>FunLike F A B<VAR>BialgHomClass 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>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<VAR>h : f.toFun 1 = 1<VAR>h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y<GOAL>⇑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = ⇑f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A → B<VAR>h₀ : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₁ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₀ }.toFun x<VAR>h₂ : Coalgebra.counit ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ } = Coalgebra.counit<VAR>h₃ : TensorProduct.map { toFun := f, map_add' := h₀, map_smul' := h₁ } { toFun := f, map_add' := h₀, map_smul' := h₁ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ }<VAR>h₄ : { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1<VAR>h₅ : ∀ (x y : A), { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y<GOAL>⇑{ toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<VAR>h : f.toFun 1 = 1<VAR>h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y<GOAL>↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₐc[R] B<GOAL>⇑↑f = ⇑f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₐc[R] B<GOAL>(↑↑f).toLinearMap = ↑f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective DFunLike.coe
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₐc[R] B<GOAL>⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective CoalgHomClass.toCoalgHom
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective AlgHomClass.toAlgHom
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective fun x => ↑x
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₐc[R] B<VAR>H : φ₁ = φ₂<VAR>x : A<GOAL>φ₁ x = φ₂ x
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₐc[R] B<VAR>x y : A<VAR>h : x = y<GOAL>φ x = φ y
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₐc[R] B<VAR>H : ∀ (x : A), φ₁ x = φ₂ x<GOAL>φ₁ = φ₂
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₐc[R] B<GOAL>φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>f g : R →ₐc[R] A<VAR>h : f 1 = g 1<GOAL>f = g
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₐc[R] B<VAR>h₀ : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₁ : ∀ (m : R) (x : A), { toFun := ⇑f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₀ }.toFun x<VAR>h₂ : Coalgebra.counit ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } = Coalgebra.counit<VAR>h₃ : TensorProduct.map { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ }<VAR>h₄ : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1<VAR>h₅ : ∀ (x y : A), { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y<GOAL>{ toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f
<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>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[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>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[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>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>a : A<GOAL>(BialgHom.id R A) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>⇑(BialgHom.id R A) = id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>↑(BialgHom.id R A) = CoalgHom.id R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>↑(BialgHom.id R A) = AlgHom.id R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<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>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₐc[R] C<VAR>φ₂ : A →ₐc[R] B<GOAL>∀ (a : A), (φ₁.comp φ₂) a = φ₁ (φ₂ a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<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>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₐc[R] C<VAR>φ₂ : A →ₐc[R] B<GOAL>⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂