ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>f : A → B<VAR>f' : B → A<VAR>h₁ : Function.LeftInverse f' f<VAR>h₂ : Function.RightInverse f' f<VAR>h₃ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)<GOAL>{ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ }.symm = let __src := StarRingEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅; { toFun := f', invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯ }
<VAR>A : Type u_1<VAR>Add A<VAR>Mul A<VAR>Star A<GOAL>StarRingEquiv.refl.symm = StarRingEquiv.refl
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<VAR>x : B<GOAL>e (e.symm x) = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<VAR>x : A<GOAL>e.symm (e x) = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>Star C<VAR>e₁ : A ≃⋆+* B<VAR>e₂ : B ≃⋆+* C<VAR>x : C<GOAL>(e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>Star C<VAR>e₁ : A ≃⋆+* B<VAR>e₂ : B ≃⋆+* C<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>Star C<VAR>e₁ : A ≃⋆+* B<VAR>e₂ : B ≃⋆+* C<VAR>x : A<GOAL>(e₁.trans e₂) x = e₂ (e₁ x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<GOAL>Function.LeftInverse ⇑e.symm ⇑e
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<GOAL>Function.RightInverse ⇑e.symm ⇑e
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalRingHomClass F A B<VAR>NonUnitalStarRingHomClass F A B<VAR>FunLike G B A<VAR>f : F<VAR>g : G<VAR>h₁ : ∀ (x : A), g (f x) = x<VAR>h₂ : ∀ (x : B), f (g x) = x<VAR>a : B<GOAL>(StarRingEquiv.ofStarRingHom f g h₁ h₂).symm a = g a
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalRingHomClass F A B<VAR>NonUnitalStarRingHomClass F A B<VAR>FunLike G B A<VAR>f : F<VAR>g : G<VAR>h₁ : ∀ (x : A), g (f x) = x<VAR>h₂ : ∀ (x : B), f (g x) = x<VAR>a : A<GOAL>(StarRingEquiv.ofStarRingHom f g h₁ h₂) a = f a
<VAR>F : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalRingHomClass F A B<VAR>NonUnitalStarRingHomClass F A B<VAR>f : F<VAR>hf : Function.Bijective ⇑f<GOAL>⇑(StarRingEquiv.ofBijective f hf) = ⇑f
<VAR>F : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalRingHomClass F A B<VAR>NonUnitalStarRingHomClass F A B<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>a : A<GOAL>(StarRingEquiv.ofBijective f hf) a = f a
<VAR>α : Type u_1<VAR>Star α<GOAL>star ∅ = ∅
<VAR>α : Type u_1<VAR>Star α<GOAL>star Set.univ = Set.univ
<VAR>α : Type u_1<VAR>InvolutiveStar α<VAR>s : Set α<GOAL>(star s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>InvolutiveStar α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>(star s).Nonempty
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Star α<GOAL>a ∈ star s ↔ star a ∈ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>InvolutiveStar α<GOAL>star a ∈ star s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Star α<GOAL>star ⁻¹' s = star s
<VAR>α : Type u_1<VAR>s : Set α<VAR>InvolutiveStar α<GOAL>star '' s = star s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Star α<GOAL>star (s ∩ t) = star s ∩ star t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Star α<GOAL>star (s ∪ t) = star s ∪ star t
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Star α<VAR>s : ι → Set α<GOAL>star (⋂ i, s i) = ⋂ i, star (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Star α<VAR>s : ι → Set α<GOAL>star (⋃ i, s i) = ⋃ i, star (s i)
<VAR>α : Type u_1<VAR>s : Set α<VAR>Star α<GOAL>star sᶜ = (star s)ᶜ
<VAR>α : Type u_1<VAR>InvolutiveStar α<VAR>s t : Set α<GOAL>star s ⊆ star t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>InvolutiveStar α<VAR>s t : Set α<GOAL>star s ⊆ t ↔ s ⊆ star t
<VAR>α : Type u_1<VAR>InvolutiveStar α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(star s).Finite
<VAR>β : Type u_2<VAR>InvolutiveStar β<VAR>x : β<GOAL>star {x} = {star x}
<VAR>α : Type u_1<VAR>Mul α<VAR>StarMul α<VAR>s t : Set α<GOAL>star (s * t) = star t * star s
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>s t : Set α<GOAL>star (s + t) = star s + star t
<VAR>α : Type u_1<VAR>Group α<VAR>StarMul α<VAR>s : Set α<GOAL>star s⁻¹ = (star s)⁻¹
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>StarRing α<VAR>s : Set α<GOAL>star s⁻¹ = (star s)⁻¹
<VAR>S : Type u_1<VAR>α : Type u_2<VAR>InvolutiveStar α<VAR>SetLike S α<VAR>StarMemClass S α<VAR>s : S<GOAL>star ↑s = ↑s
<VAR>α : Type u_1<VAR>x : α<GOAL>star (FreeMonoid.of x) = FreeMonoid.of x
<VAR>α : Type u_1<GOAL>star 1 = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>x : X<GOAL>star (FreeAlgebra.ι R x) = FreeAlgebra.ι R x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>X : Type u_2<VAR>r : R<GOAL>star ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)) r
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<GOAL>IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<GOAL>IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>NoZeroDivisors R<GOAL>¬IsPrimePow 0
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<VAR>h : IsPrimePow n<GOAL>¬IsUnit n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<VAR>h : IsUnit n<GOAL>¬IsPrimePow n
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<GOAL>¬IsPrimePow 1
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>p : R<VAR>hp : Prime p<GOAL>IsPrimePow p
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<VAR>hn : IsPrimePow n<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>IsPrimePow (n ^ k)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>NoZeroDivisors R<VAR>n : R<VAR>h : IsPrimePow n<GOAL>n ≠ 0
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>n : R<VAR>h : IsPrimePow n<GOAL>n ≠ 1
<VAR>n : ℕ<GOAL>IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>IsPrimePow p
<VAR>n : ℕ<GOAL>IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>n m : ℕ<VAR>hn : IsPrimePow n<VAR>hm : m ∣ n<VAR>hm₁ : m ≠ 1<GOAL>IsPrimePow m
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)
<VAR>n : ℕ<GOAL>IsPrimePow n → 2 ≤ n
<VAR>n : ℕ<VAR>hn : IsPrimePow n<GOAL>0 < n
<VAR>n : ℕ<VAR>h : IsPrimePow n<GOAL>1 < n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>self : CharZero R<GOAL>Function.Injective Nat.cast
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>H : ∀ (n : ℕ), ↑n = 0 → n = 0<GOAL>CharZero R
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<GOAL>Function.Injective Nat.cast
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>m n : ℕ<GOAL>↑m = ↑n ↔ m = n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<GOAL>↑n = 0 ↔ n = 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<GOAL>↑n ≠ 0 ↔ n ≠ 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<GOAL>↑n + 1 ≠ 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<GOAL>↑n = 1 ↔ n = 1
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<GOAL>↑n ≠ 1 ↔ n ≠ 1
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≠ 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>0 ≠ OfNat.ofNat n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ≠ 1
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>1 ≠ OfNat.ofNat n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<VAR>m n : ℕ<VAR>m.AtLeastTwo<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : MvPolynomial PUnit.{u_2 + 1} R<GOAL>(MvPolynomial.pUnitAlgEquiv R) p = MvPolynomial.eval₂ Polynomial.C (fun x => Polynomial.X) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : R[X]<GOAL>(MvPolynomial.pUnitAlgEquiv R).symm p = Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X PUnit.unit) p
<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>e : S₁ ≃+* S₂<VAR>a : MvPolynomial σ S₁<GOAL>(MvPolynomial.mapEquiv σ e) a = (MvPolynomial.map ↑e) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl (MvPolynomial σ R)
<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>σ : Type u_1<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>e : S₁ ≃+* S₂<GOAL>(MvPolynomial.mapEquiv σ e).symm = MvPolynomial.mapEquiv σ e.symm
<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>CommSemiring S₁<VAR>CommSemiring S₂<VAR>CommSemiring S₃<VAR>e : S₁ ≃+* S₂<VAR>f : S₂ ≃+* S₃<GOAL>(MvPolynomial.mapEquiv σ e).trans (MvPolynomial.mapEquiv σ f) = MvPolynomial.mapEquiv σ (e.trans f)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A₁ : Type u_2<VAR>A₂ : Type u_3<VAR>CommSemiring A₁<VAR>CommSemiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<VAR>a : MvPolynomial σ A₁<GOAL>(MvPolynomial.mapAlgEquiv σ e) a = (MvPolynomial.map ↑e) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A₁ : Type u_2<VAR>CommSemiring A₁<VAR>Algebra R A₁<GOAL>MvPolynomial.mapAlgEquiv σ AlgEquiv.refl = AlgEquiv.refl
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A₁ : Type u_2<VAR>A₂ : Type u_3<VAR>CommSemiring A₁<VAR>CommSemiring A₂<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>e : A₁ ≃ₐ[R] A₂<GOAL>(MvPolynomial.mapAlgEquiv σ e).symm = MvPolynomial.mapAlgEquiv σ e.symm
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>A₁ : Type u_2<VAR>A₂ : Type u_3<VAR>A₃ : Type u_4<VAR>CommSemiring A₁<VAR>CommSemiring A₂<VAR>CommSemiring A₃<VAR>Algebra R A₁<VAR>Algebra R A₂<VAR>Algebra R A₃<VAR>e : A₁ ≃ₐ[R] A₂<VAR>f : A₂ ≃ₐ[R] A₃<GOAL>(MvPolynomial.mapAlgEquiv σ e).trans (MvPolynomial.mapAlgEquiv σ f) = MvPolynomial.mapAlgEquiv σ (e.trans f)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>a : R<GOAL>(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.C a) = MvPolynomial.C (MvPolynomial.C a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>b : S₁<GOAL>(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inl b)) = MvPolynomial.X b
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>c : S₂<GOAL>(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inr c)) = MvPolynomial.C (MvPolynomial.X c)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>a : R<GOAL>(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.C a)) = MvPolynomial.C a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>b : S₁<GOAL>(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.X b) = MvPolynomial.X (Sum.inl b)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>c : S₂<GOAL>(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.X c)) = MvPolynomial.X (Sum.inr c)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>he : IsEmpty σ<VAR>a : MvPolynomial σ R<GOAL>(MvPolynomial.isEmptyAlgEquiv R σ) a = (MvPolynomial.aeval fun a => he.elim a) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>he : IsEmpty σ<VAR>a : R<VAR>j : σ →₀ ℕ<GOAL>((MvPolynomial.isEmptyAlgEquiv R σ).symm a) j = Pi.single 0 a j
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>he : IsEmpty σ<VAR>a : R<GOAL>((MvPolynomial.isEmptyAlgEquiv R σ).symm a).support = if a = 0 then ∅ else {0}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>IsEmpty σ<VAR>a : R<GOAL>((MvPolynomial.isEmptyRingEquiv R σ).symm a).support = if a = 0 then ∅ else {0}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>IsEmpty σ<VAR>a : MvPolynomial σ R<GOAL>(MvPolynomial.isEmptyRingEquiv R σ) a = (MvPolynomial.aeval fun a => inst✝.elim a) a
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>IsEmpty σ<VAR>a : R<VAR>j : σ →₀ ℕ<GOAL>((MvPolynomial.isEmptyRingEquiv R σ).symm a) j = Pi.single 0 a j
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>CommSemiring R<VAR>CommSemiring S₃<VAR>f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃<VAR>g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R<VAR>hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C<VAR>hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n<VAR>hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C<VAR>hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n<VAR>a : MvPolynomial S₁ R<GOAL>(MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>CommSemiring R<VAR>CommSemiring S₃<VAR>f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃<VAR>g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R<VAR>hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C<VAR>hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n<VAR>hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C<VAR>hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n<VAR>a : MvPolynomial S₂ S₃<GOAL>(MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).symm a = g a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>a : MvPolynomial S₁ (MvPolynomial S₂ R)<GOAL>(MvPolynomial.sumAlgEquiv R S₁ S₂).symm a = (MvPolynomial.iterToSum R S₁ S₂) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>CommSemiring R<VAR>a : MvPolynomial (S₁ ⊕ S₂) R<GOAL>(MvPolynomial.sumAlgEquiv R S₁ S₂) a = (MvPolynomial.sumToIter R S₁ S₂) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>a : (MvPolynomial S₁ R)[X]<GOAL>(MvPolynomial.optionEquivLeft R S₁).symm a = (Polynomial.aevalTower (MvPolynomial.rename some) (MvPolynomial.X none)) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>a : MvPolynomial (Option S₁) R<GOAL>(MvPolynomial.optionEquivLeft R S₁) a = (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>x : S₁<GOAL>(MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.X (some x)) = Polynomial.C (MvPolynomial.X x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<GOAL>(MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.X none) = Polynomial.X
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>r : R<GOAL>(MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.C r) = Polynomial.C (MvPolynomial.C r)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>a : MvPolynomial (Option S₁) R<GOAL>(MvPolynomial.optionEquivRight R S₁) a = (MvPolynomial.aeval fun o => o.elim (MvPolynomial.C Polynomial.X) MvPolynomial.X) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>a : MvPolynomial S₁ R[X]<GOAL>(MvPolynomial.optionEquivRight R S₁).symm a = (MvPolynomial.aevalTower (Polynomial.aeval (MvPolynomial.X none)) fun i => MvPolynomial.X (some i)) a
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>x : S₁<GOAL>(MvPolynomial.optionEquivRight R S₁) (MvPolynomial.X (some x)) = MvPolynomial.X x
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<GOAL>(MvPolynomial.optionEquivRight R S₁) (MvPolynomial.X none) = MvPolynomial.C Polynomial.X
<VAR>R : Type u<VAR>S₁ : Type v<VAR>CommSemiring R<VAR>r : R<GOAL>(MvPolynomial.optionEquivRight R S₁) (MvPolynomial.C r) = MvPolynomial.C (Polynomial.C r)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<GOAL>↑(MvPolynomial.finSuccEquiv R n) = MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<GOAL>(MvPolynomial.finSuccEquiv R n) p = (MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<GOAL>(↑(MvPolynomial.finSuccEquiv R n).symm).comp (Polynomial.C.comp MvPolynomial.C) = MvPolynomial.C
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<GOAL>(MvPolynomial.finSuccEquiv R n) (MvPolynomial.X 0) = Polynomial.X
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>j : Fin n<GOAL>(MvPolynomial.finSuccEquiv R n) (MvPolynomial.X j.succ) = Polynomial.C (MvPolynomial.X j)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>m : Fin n →₀ ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<GOAL>MvPolynomial.coeff m (((MvPolynomial.finSuccEquiv R n) f).coeff i) = MvPolynomial.coeff (Finsupp.cons i m) f
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<GOAL>(MvPolynomial.eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (MvPolynomial.eval s) ((MvPolynomial.finSuccEquiv R n) f))
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>s' : Fin n → R<VAR>f : (MvPolynomial (Fin n) R)[X]<VAR>i : ℕ<GOAL>(Polynomial.map (MvPolynomial.eval s') f).coeff i = (MvPolynomial.eval s') (f.coeff i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>m : Fin n →₀ ℕ<GOAL>m ∈ (((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i m ∈ f.support
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((MvPolynomial.finSuccEquiv R n) f).coeff i ≠ 0<GOAL>(((MvPolynomial.finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<GOAL>((MvPolynomial.finSuccEquiv R n) f).support = Finset.image (fun m => m 0) f.support
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<GOAL>Finset.image (Finsupp.cons i) (((MvPolynomial.finSuccEquiv R n) f).coeff i).support = Finset.filter (fun m => m 0 = i) f.support
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>h : f ≠ 0<GOAL>((MvPolynomial.finSuccEquiv R n) f).support.Nonempty
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>h : f ≠ 0<GOAL>((MvPolynomial.finSuccEquiv R n) f).degree = ↑(MvPolynomial.degreeOf 0 f)
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<GOAL>((MvPolynomial.finSuccEquiv R n) f).natDegree = MvPolynomial.degreeOf 0 f
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<VAR>j : Fin n<VAR>i : ℕ<GOAL>MvPolynomial.degreeOf j (((MvPolynomial.finSuccEquiv R n) p).coeff i) ≤ MvPolynomial.degreeOf j.succ p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<VAR>e : σ ≃ Fin n<VAR>φ : MvPolynomial (Option σ) R<GOAL>(MvPolynomial.finSuccEquiv R n) ((MvPolynomial.rename ⇑(e.optionCongr.trans (finSuccEquiv n).symm)) φ) = Polynomial.map (MvPolynomial.rename ⇑e).toRingHom ((MvPolynomial.optionEquivLeft R σ) φ)
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>CharZero R<GOAL>∀ (a : ℕ), Nat.castEmbedding a = ↑a
<VAR>R : Type u_2<VAR>Semiring R<VAR>CharZero R<VAR>q n : ℕ<VAR>hn : n ≠ 0<GOAL>↑q ^ n = 1 ↔ q = 1
<VAR>k : Type u_2<VAR>DivisionSemiring k<VAR>CharZero k<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddMonoidWithOne M<VAR>CharZero M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Function.support ↑n = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddMonoidWithOne M<VAR>CharZero M<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>Function.mulSupport ↑n = Set.univ
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>a : R<GOAL>a + a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>a : R<GOAL>-a = a ↔ a = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>a : R<GOAL>a = -a ↔ a = 0
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>n : ℕ<VAR>a b : R<VAR>h : ↑n * a = ↑n * b<GOAL>n = 0 ∨ a = b
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>n : ℕ<VAR>a b : R<VAR>h : ↑n * a = ↑n * b<VAR>w : n ≠ 0<GOAL>a = b
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>NeZero 2<VAR>a : R<GOAL>(a + a) / 2 = a
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>NeZero 2<VAR>a : R<GOAL>a / 2 + a / 2 = a
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>a : R<GOAL>a - a / 2 = a / 2
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>a : R<GOAL>a / 2 - a = -(a / 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>ϕ : R →+* S<VAR>CharZero S<GOAL>CharZero R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>ϕ : R →+* S<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>CharZero R ↔ CharZero S
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>f : ℕ →+* R<VAR>CharZero R<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>Ring R<VAR>CharZero R<VAR>u : Rˣ<GOAL>u ≠ -u
<VAR>R : Type u_1<VAR>Ring R<VAR>CharZero R<VAR>u : Rˣ<GOAL>-u ≠ u
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>p r : R<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>z • r ∈ AddSubgroup.zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>p r : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • r ∈ AddSubgroup.zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ AddSubgroup.zmultiples p
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>p : R<VAR>ψ θ : R ⧸ AddSubgroup.zmultiples p<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>p : R<VAR>ψ θ : R ⧸ AddSubgroup.zmultiples p<VAR>n : ℕ<VAR>hz : n ≠ 0<GOAL>n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>self : StarOrderedRing R<VAR>x y : R<GOAL>x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s<GOAL>StarOrderedRing R
<VAR>R : Type u<VAR>NonUnitalRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y<VAR>h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)<GOAL>StarOrderedRing R
<VAR>R : Type u<VAR>NonUnitalRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y<VAR>h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s<GOAL>StarOrderedRing R
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>r : R<GOAL>0 ≤ star r * r
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>r : R<GOAL>0 ≤ r * star r
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>c : R<GOAL>0 ≤ star c * a * c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>c : R<GOAL>0 ≤ c * a * star c