diff --git a/Mathbin/Data/MvPolynomial/Basic.lean b/Mathbin/Data/MvPolynomial/Basic.lean index 7e1ea5544d..4513e5119c 100644 --- a/Mathbin/Data/MvPolynomial/Basic.lean +++ b/Mathbin/Data/MvPolynomial/Basic.lean @@ -2433,6 +2433,12 @@ variable [Algebra R S₁] [CommSemiring S₂] variable (f : σ → S₁) +/- warning: mv_polynomial.algebra_map_apply -> MvPolynomial.algebraMap_apply is a dubious translation: +lean 3 declaration is + forall {R : Type.{u1}} {S₁ : Type.{u2}} {σ : Type.{u3}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : CommSemiring.{u2} S₁] [_inst_3 : Algebra.{u1, u2} R S₁ _inst_1 (CommSemiring.toSemiring.{u2} S₁ _inst_2)] (r : R), Eq.{max (succ u3) (succ u2)} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (coeFn.{max (succ u1) (succ (max u3 u2)), max (succ u1) (succ (max u3 u2))} (RingHom.{u1, max u3 u2} R (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) (fun (_x : RingHom.{u1, max u3 u2} R (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) => R -> (MvPolynomial.{u3, u2} σ S₁ _inst_2)) (RingHom.hasCoeToFun.{u1, max u3 u2} R (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) (algebraMap.{u1, max u3 u2} R (MvPolynomial.{u3, u2} σ S₁ _inst_2) _inst_1 (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)) (MvPolynomial.algebra.{u1, u2, u3} R S₁ σ _inst_1 _inst_2 _inst_3)) r) (coeFn.{max (succ u2) (succ (max u3 u2)), max (succ u2) (succ (max u3 u2))} (RingHom.{u2, max u3 u2} S₁ (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) (fun (_x : RingHom.{u2, max u3 u2} S₁ (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) => S₁ -> (MvPolynomial.{u3, u2} σ S₁ _inst_2)) (RingHom.hasCoeToFun.{u2, max u3 u2} S₁ (MvPolynomial.{u3, u2} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u2} (MvPolynomial.{u3, u2} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u2, u3} S₁ σ _inst_2)))) (MvPolynomial.C.{u2, u3} S₁ σ _inst_2) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) (fun (_x : RingHom.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) => R -> S₁) (RingHom.hasCoeToFun.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) (algebraMap.{u1, u2} R S₁ _inst_1 (CommSemiring.toSemiring.{u2} S₁ _inst_2) _inst_3) r)) +but is expected to have type + forall {R : Type.{u2}} {S₁ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_2 : CommSemiring.{u3} S₁] [_inst_3 : Algebra.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2)] (r : R), Eq.{max (succ u3) (succ u1)} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MvPolynomial.{u1, u3} σ S₁ _inst_2) r) (FunLike.coe.{max (max (succ u2) (succ u3)) (succ u1), succ u2, max (succ u3) (succ u1)} (RingHom.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => MvPolynomial.{u1, u3} σ S₁ _inst_2) _x) (MulHomClass.toFunLike.{max (max u2 u3) u1, u2, max u3 u1} (RingHom.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)))) R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2))))) (NonUnitalRingHomClass.toMulHomClass.{max (max u2 u3) u1, u2, max u3 u1} (RingHom.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)))) R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)))) (RingHomClass.toNonUnitalRingHomClass.{max (max u2 u3) u1, u2, max u3 u1} (RingHom.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)))) R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2))) (RingHom.instRingHomClassRingHom.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2))))))) (algebraMap.{u2, max u3 u1} R (MvPolynomial.{u1, u3} σ S₁ _inst_2) _inst_1 (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ S₁ _inst_2) (MvPolynomial.commSemiring.{u3, u1} S₁ σ _inst_2)) (MvPolynomial.algebra.{u2, u3, u1} R S₁ σ _inst_1 _inst_2 _inst_3)) r) (FunLike.coe.{max (succ u1) (succ u3), succ u3, max (succ u1) (succ u3)} (RingHom.{u3, max u3 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2)))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (fun (_x : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) => MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) _x) (MulHomClass.toFunLike.{max u1 u3, u3, max u1 u3} (RingHom.{u3, max u3 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2)))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (NonUnitalNonAssocSemiring.toMul.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)))) (NonUnitalNonAssocSemiring.toMul.{max u1 u3} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u3} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2))))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u3, u3, max u1 u3} (RingHom.{u3, max u3 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2)))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u3} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2)))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u3, u3, max u1 u3} (RingHom.{u3, max u3 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2)))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2))) (RingHom.instRingHomClassRingHom.{u3, max u1 u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (Semiring.toNonAssocSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) (CommSemiring.toSemiring.{u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2)) (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u1, u3} σ ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) _inst_2) (MvPolynomial.commSemiring.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2))))))) (MvPolynomial.C.{u3, u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) r) σ _inst_2) (FunLike.coe.{max (succ u2) (succ u3), succ u2, succ u3} (RingHom.{u2, u3} R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₁) _x) (MulHomClass.toFunLike.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) R S₁ (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) R S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)) (RingHom.instRingHomClassRingHom.{u2, u3} R S₁ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (algebraMap.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3) r)) +Case conversion may be inaccurate. Consider using '#align mv_polynomial.algebra_map_apply MvPolynomial.algebraMap_applyₓ'. -/ theorem algebraMap_apply (r : R) : algebraMap R (MvPolynomial σ S₁) r = C (algebraMap R S₁ r) := rfl #align mv_polynomial.algebra_map_apply MvPolynomial.algebraMap_apply @@ -2550,7 +2556,7 @@ theorem map_aeval {B : Type _} [CommSemiring B] (g : σ → S₁) (φ : S₁ → lean 3 declaration is forall {R : Type.{u1}} {S₂ : Type.{u2}} {σ : Type.{u3}} [_inst_1 : CommSemiring.{u1} R] [_inst_4 : CommSemiring.{u2} S₂] (f : RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))), Eq.{max (succ (max u3 u1)) (succ u2)} (RingHom.{max u3 u1, u2} (MvPolynomial.{u3, u1} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (MvPolynomial.eval₂Hom.{u1, u2, u3} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u2} (σ -> S₂) 0 (OfNat.mk.{max u3 u2} (σ -> S₂) 0 (Zero.zero.{max u3 u2} (σ -> S₂) (Pi.instZero.{u3, u2} σ (fun (ᾰ : σ) => S₂) (fun (i : σ) => MulZeroClass.toHasZero.{u2} S₂ (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S₂ (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4)))))))))) (RingHom.comp.{max u3 u1, u1, u2} (MvPolynomial.{u3, u1} σ R _inst_1) R S₂ (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4)) f (MvPolynomial.constantCoeff.{u1, u3} R σ _inst_1)) but is expected to have type - forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))), Eq.{max (max (succ u2) (succ u3)) (succ u1)} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.eval₂Hom.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.19995 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4)))))) (RingHom.comp.{max u1 u2, u2, u3} (MvPolynomial.{u1, u2} σ R _inst_1) R S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) f (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1)) + forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))), Eq.{max (max (succ u2) (succ u3)) (succ u1)} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.eval₂Hom.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20063 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4)))))) (RingHom.comp.{max u1 u2, u2, u3} (MvPolynomial.{u1, u2} σ R _inst_1) R S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) f (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1)) Case conversion may be inaccurate. Consider using '#align mv_polynomial.eval₂_hom_zero MvPolynomial.eval₂Hom_zeroₓ'. -/ @[simp] theorem eval₂Hom_zero (f : R →+* S₂) : eval₂Hom f (0 : σ → S₂) = f.comp constantCoeff := by @@ -2572,7 +2578,7 @@ theorem eval₂Hom_zero' (f : R →+* S₂) : eval₂Hom f (fun _ => 0 : σ → lean 3 declaration is forall {R : Type.{u1}} {S₂ : Type.{u2}} {σ : Type.{u3}} [_inst_1 : CommSemiring.{u1} R] [_inst_4 : CommSemiring.{u2} S₂] (f : RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (p : MvPolynomial.{u3, u1} σ R _inst_1), Eq.{succ u2} S₂ (coeFn.{max (succ (max u3 u1)) (succ u2), max (succ (max u3 u1)) (succ u2)} (RingHom.{max u3 u1, u2} (MvPolynomial.{u3, u1} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (fun (_x : RingHom.{max u3 u1, u2} (MvPolynomial.{u3, u1} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) => (MvPolynomial.{u3, u1} σ R _inst_1) -> S₂) (RingHom.hasCoeToFun.{max u3 u1, u2} (MvPolynomial.{u3, u1} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (MvPolynomial.eval₂Hom.{u1, u2, u3} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u2} (σ -> S₂) 0 (OfNat.mk.{max u3 u2} (σ -> S₂) 0 (Zero.zero.{max u3 u2} (σ -> S₂) (Pi.instZero.{u3, u2} σ (fun (ᾰ : σ) => S₂) (fun (i : σ) => MulZeroClass.toHasZero.{u2} S₂ (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S₂ (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4)))))))))) p) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (fun (_x : RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) => R -> S₂) (RingHom.hasCoeToFun.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) f (coeFn.{max (succ (max u3 u1)) (succ u1), max (succ (max u3 u1)) (succ u1)} (RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (fun (_x : RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) => (MvPolynomial.{u3, u1} σ R _inst_1) -> R) (RingHom.hasCoeToFun.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (MvPolynomial.constantCoeff.{u1, u3} R σ _inst_1) p)) but is expected to have type - forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => S₂) p) (FunLike.coe.{max (max (succ u2) (succ u3)) (succ u1), max (succ u2) (succ u1), succ u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => S₂) _x) (MulHomClass.toFunLike.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) (MvPolynomial.eval₂Hom.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20149 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4)))))) p) (FunLike.coe.{max (succ u2) (succ u3), succ u2, succ u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₂) _x) (MulHomClass.toFunLike.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) f (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) + forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => S₂) p) (FunLike.coe.{max (max (succ u2) (succ u3)) (succ u1), max (succ u2) (succ u1), succ u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => S₂) _x) (MulHomClass.toFunLike.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max (max u2 u3) u1, max u2 u1, u3} (RingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{max u2 u1, u3} (MvPolynomial.{u1, u2} σ R _inst_1) S₂ (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) (MvPolynomial.eval₂Hom.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20217 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4)))))) p) (FunLike.coe.{max (succ u2) (succ u3), succ u2, succ u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₂) _x) (MulHomClass.toFunLike.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) f (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) Case conversion may be inaccurate. Consider using '#align mv_polynomial.eval₂_hom_zero_apply MvPolynomial.eval₂Hom_zero_applyₓ'. -/ theorem eval₂Hom_zero_apply (f : R →+* S₂) (p : MvPolynomial σ R) : eval₂Hom f (0 : σ → S₂) p = f (constantCoeff p) := @@ -2594,7 +2600,7 @@ theorem eval₂Hom_zero'_apply (f : R →+* S₂) (p : MvPolynomial σ R) : lean 3 declaration is forall {R : Type.{u1}} {S₂ : Type.{u2}} {σ : Type.{u3}} [_inst_1 : CommSemiring.{u1} R] [_inst_4 : CommSemiring.{u2} S₂] (f : RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (p : MvPolynomial.{u3, u1} σ R _inst_1), Eq.{succ u2} S₂ (MvPolynomial.eval₂.{u1, u2, u3} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u2} (σ -> S₂) 0 (OfNat.mk.{max u3 u2} (σ -> S₂) 0 (Zero.zero.{max u3 u2} (σ -> S₂) (Pi.instZero.{u3, u2} σ (fun (ᾰ : σ) => S₂) (fun (i : σ) => MulZeroClass.toHasZero.{u2} S₂ (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S₂ (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))))))))) p) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) (fun (_x : RingHom.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) => R -> S₂) (RingHom.hasCoeToFun.{u1, u2} R S₂ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₂ (CommSemiring.toSemiring.{u2} S₂ _inst_4))) f (coeFn.{max (succ (max u3 u1)) (succ u1), max (succ (max u3 u1)) (succ u1)} (RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (fun (_x : RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) => (MvPolynomial.{u3, u1} σ R _inst_1) -> R) (RingHom.hasCoeToFun.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (MvPolynomial.constantCoeff.{u1, u3} R σ _inst_1) p)) but is expected to have type - forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} S₂ (MvPolynomial.eval₂.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20308 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4))))) p) (FunLike.coe.{max (succ u2) (succ u3), succ u2, succ u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₂) _x) (MulHomClass.toFunLike.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) f (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) + forall {R : Type.{u2}} {S₂ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_4 : CommSemiring.{u3} S₂] (f : RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} S₂ (MvPolynomial.eval₂.{u2, u3, u1} R S₂ σ _inst_1 _inst_4 f (OfNat.ofNat.{max u3 u1} (σ -> S₂) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₂) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20376 : σ) => S₂) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₂ (CommSemiring.toCommMonoidWithZero.{u3} S₂ _inst_4))))) p) (FunLike.coe.{max (succ u2) (succ u3), succ u2, succ u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => S₂) _x) (MulHomClass.toFunLike.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₂ (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u3, u2, u3} (RingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4))) R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)) (RingHom.instRingHomClassRingHom.{u2, u3} R S₂ (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₂ (CommSemiring.toSemiring.{u3} S₂ _inst_4)))))) f (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) Case conversion may be inaccurate. Consider using '#align mv_polynomial.eval₂_zero_apply MvPolynomial.eval₂_zero_applyₓ'. -/ @[simp] theorem eval₂_zero_apply (f : R →+* S₂) (p : MvPolynomial σ R) : @@ -2618,7 +2624,7 @@ theorem eval₂_zero'_apply (f : R →+* S₂) (p : MvPolynomial σ R) : lean 3 declaration is forall {R : Type.{u1}} {S₁ : Type.{u2}} {σ : Type.{u3}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : CommSemiring.{u2} S₁] [_inst_3 : Algebra.{u1, u2} R S₁ _inst_1 (CommSemiring.toSemiring.{u2} S₁ _inst_2)] (p : MvPolynomial.{u3, u1} σ R _inst_1), Eq.{succ u2} S₁ (coeFn.{max (succ (max u3 u1)) (succ u2), max (succ (max u3 u1)) (succ u2)} (AlgHom.{u1, max u3 u1, u2} R (MvPolynomial.{u3, u1} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1)) (CommSemiring.toSemiring.{u2} S₁ _inst_2) (MvPolynomial.algebra.{u1, u1, u3} R R σ _inst_1 _inst_1 (Algebra.id.{u1} R _inst_1)) _inst_3) (fun (_x : AlgHom.{u1, max u3 u1, u2} R (MvPolynomial.{u3, u1} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1)) (CommSemiring.toSemiring.{u2} S₁ _inst_2) (MvPolynomial.algebra.{u1, u1, u3} R R σ _inst_1 _inst_1 (Algebra.id.{u1} R _inst_1)) _inst_3) => (MvPolynomial.{u3, u1} σ R _inst_1) -> S₁) ([anonymous].{u1, max u3 u1, u2} R (MvPolynomial.{u3, u1} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1)) (CommSemiring.toSemiring.{u2} S₁ _inst_2) (MvPolynomial.algebra.{u1, u1, u3} R R σ _inst_1 _inst_1 (Algebra.id.{u1} R _inst_1)) _inst_3) (MvPolynomial.aeval.{u1, u2, u3} R S₁ σ _inst_1 _inst_2 _inst_3 (OfNat.ofNat.{max u3 u2} (σ -> S₁) 0 (OfNat.mk.{max u3 u2} (σ -> S₁) 0 (Zero.zero.{max u3 u2} (σ -> S₁) (Pi.instZero.{u3, u2} σ (fun (ᾰ : σ) => S₁) (fun (i : σ) => MulZeroClass.toHasZero.{u2} S₁ (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} S₁ (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2)))))))))) p) (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (RingHom.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) (fun (_x : RingHom.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) => R -> S₁) (RingHom.hasCoeToFun.{u1, u2} R S₁ (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{u2} S₁ (CommSemiring.toSemiring.{u2} S₁ _inst_2))) (algebraMap.{u1, u2} R S₁ _inst_1 (CommSemiring.toSemiring.{u2} S₁ _inst_2) _inst_3) (coeFn.{max (succ (max u3 u1)) (succ u1), max (succ (max u3 u1)) (succ u1)} (RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (fun (_x : RingHom.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) => (MvPolynomial.{u3, u1} σ R _inst_1) -> R) (RingHom.hasCoeToFun.{max u3 u1, u1} (MvPolynomial.{u3, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u3 u1} (MvPolynomial.{u3, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u3} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (MvPolynomial.constantCoeff.{u1, u3} R σ _inst_1) p)) but is expected to have type - forall {R : Type.{u2}} {S₁ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_2 : CommSemiring.{u3} S₁] [_inst_3 : Algebra.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2)] (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : MvPolynomial.{u1, u2} σ R _inst_1) => S₁) p) (FunLike.coe.{max (max (succ u3) (succ u1)) (succ u2), max (succ u1) (succ u2), succ u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : MvPolynomial.{u1, u2} σ R _inst_1) => S₁) _x) (SMulHomClass.toFunLike.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (SMulZeroClass.toSMul.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (AddMonoid.toZero.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))))) (DistribSMul.toSMulZeroClass.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (AddMonoid.toAddZeroClass.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))))) (DistribMulAction.toDistribSMul.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1))))))) (SMulZeroClass.toSMul.{u2, u3} R S₁ (AddMonoid.toZero.{u3} S₁ (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (DistribSMul.toSMulZeroClass.{u2, u3} R S₁ (AddMonoid.toAddZeroClass.{u3} S₁ (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (DistribMulAction.toDistribSMul.{u2, u3} R S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3))))) (DistribMulActionHomClass.toSMulHomClass.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))))) (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3)) (NonUnitalAlgHomClass.toDistribMulActionHomClass.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3)) (AlgHom.instNonUnitalAlgHomClassToMonoidToMonoidWithZeroToSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToDistribMulActionToAddCommMonoidToModuleToDistribMulActionToAddCommMonoidToModule.{u2, max u1 u2, u3, max (max u3 u1) u2} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3 (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) (AlgHom.algHomClass.{u2, max u1 u2, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3))))) (MvPolynomial.aeval.{u2, u3, u1} R S₁ σ _inst_1 _inst_2 _inst_3 (OfNat.ofNat.{max u3 u1} (σ -> S₁) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₁) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20456 : σ) => S₁) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₁ (CommSemiring.toCommMonoidWithZero.{u3} S₁ _inst_2)))))) p) (FunLike.coe.{max (succ u3) (succ u2), succ u2, succ u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (fun (_x : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) => S₁) _x) (MulHomClass.toFunLike.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (NonUnitalNonAssocSemiring.toMul.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (NonUnitalRingHomClass.toMulHomClass.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) (RingHomClass.toNonUnitalRingHomClass.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)) (RingHom.instRingHomClassRingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (algebraMap.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3) (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) + forall {R : Type.{u2}} {S₁ : Type.{u3}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R] [_inst_2 : CommSemiring.{u3} S₁] [_inst_3 : Algebra.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2)] (p : MvPolynomial.{u1, u2} σ R _inst_1), Eq.{succ u3} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : MvPolynomial.{u1, u2} σ R _inst_1) => S₁) p) (FunLike.coe.{max (max (succ u3) (succ u1)) (succ u2), max (succ u1) (succ u2), succ u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : MvPolynomial.{u1, u2} σ R _inst_1) => S₁) _x) (SMulHomClass.toFunLike.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (SMulZeroClass.toSMul.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (AddMonoid.toZero.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))))) (DistribSMul.toSMulZeroClass.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (AddMonoid.toAddZeroClass.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))))) (DistribMulAction.toDistribSMul.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1))))))) (SMulZeroClass.toSMul.{u2, u3} R S₁ (AddMonoid.toZero.{u3} S₁ (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (DistribSMul.toSMulZeroClass.{u2, u3} R S₁ (AddMonoid.toAddZeroClass.{u3} S₁ (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (DistribMulAction.toDistribSMul.{u2, u3} R S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3))))) (DistribMulActionHomClass.toSMulHomClass.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (AddCommMonoid.toAddMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))))) (AddCommMonoid.toAddMonoid.{u3} S₁ (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3)) (NonUnitalAlgHomClass.toDistribMulActionHomClass.{max (max u3 u1) u2, u2, max u1 u2, u3} (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ (MonoidWithZero.toMonoid.{u2} R (Semiring.toMonoidWithZero.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) (Module.toDistribMulAction.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (Algebra.toModule.{u2, max u1 u2} R (MvPolynomial.{u1, u2} σ R _inst_1) _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)))) (Module.toDistribMulAction.{u2, u3} R S₁ (CommSemiring.toSemiring.{u2} R _inst_1) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (Algebra.toModule.{u2, u3} R S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3)) (AlgHom.instNonUnitalAlgHomClassToMonoidToMonoidWithZeroToSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToDistribMulActionToAddCommMonoidToModuleToDistribMulActionToAddCommMonoidToModule.{u2, max u1 u2, u3, max (max u3 u1) u2} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3 (AlgHom.{u2, max u2 u1, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3) (AlgHom.algHomClass.{u2, max u1 u2, u3} R (MvPolynomial.{u1, u2} σ R _inst_1) S₁ _inst_1 (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)) (CommSemiring.toSemiring.{u3} S₁ _inst_2) (MvPolynomial.algebra.{u2, u2, u1} R R σ _inst_1 _inst_1 (Algebra.id.{u2} R _inst_1)) _inst_3))))) (MvPolynomial.aeval.{u2, u3, u1} R S₁ σ _inst_1 _inst_2 _inst_3 (OfNat.ofNat.{max u3 u1} (σ -> S₁) 0 (Zero.toOfNat0.{max u3 u1} (σ -> S₁) (Pi.instZero.{u1, u3} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20524 : σ) => S₁) (fun (i : σ) => CommMonoidWithZero.toZero.{u3} S₁ (CommSemiring.toCommMonoidWithZero.{u3} S₁ _inst_2)))))) p) (FunLike.coe.{max (succ u3) (succ u2), succ u2, succ u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (fun (_x : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) => S₁) _x) (MulHomClass.toFunLike.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (NonUnitalNonAssocSemiring.toMul.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{u3} S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))) (NonUnitalRingHomClass.toMulHomClass.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u3} S₁ (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) (RingHomClass.toNonUnitalRingHomClass.{max u3 u2, u2, u3} (RingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2))) ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)) (RingHom.instRingHomClassRingHom.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ (Semiring.toNonAssocSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) (CommSemiring.toSemiring.{u2} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) _inst_1)) (Semiring.toNonAssocSemiring.{u3} S₁ (CommSemiring.toSemiring.{u3} S₁ _inst_2)))))) (algebraMap.{u2, u3} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) p) S₁ _inst_1 (CommSemiring.toSemiring.{u3} S₁ _inst_2) _inst_3) (FunLike.coe.{max (succ u1) (succ u2), max (succ u1) (succ u2), succ u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) (fun (_x : MvPolynomial.{u1, u2} σ R _inst_1) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : MvPolynomial.{u1, u2} σ R _inst_1) => R) _x) (MulHomClass.toFunLike.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonUnitalNonAssocSemiring.toMul.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))))) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalRingHomClass.toMulHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (MvPolynomial.{u1, u2} σ R _inst_1) (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1)))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (RingHomClass.toNonUnitalRingHomClass.{max u1 u2, max u1 u2, u2} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (RingHom.instRingHomClassRingHom.{max u1 u2, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) p)) Case conversion may be inaccurate. Consider using '#align mv_polynomial.aeval_zero MvPolynomial.aeval_zeroₓ'. -/ @[simp] theorem aeval_zero (p : MvPolynomial σ R) : @@ -2642,7 +2648,7 @@ theorem aeval_zero' (p : MvPolynomial σ R) : lean 3 declaration is forall {R : Type.{u1}} {σ : Type.{u2}} [_inst_1 : CommSemiring.{u1} R], Eq.{max (succ (max u2 u1)) (succ u1)} (RingHom.{max u2 u1, u1} (MvPolynomial.{u2, u1} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u2, u1} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u2, u1} σ R _inst_1) (MvPolynomial.commSemiring.{u1, u2} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1))) (MvPolynomial.eval.{u1, u2} R σ _inst_1 (OfNat.ofNat.{max u2 u1} (σ -> R) 0 (OfNat.mk.{max u2 u1} (σ -> R) 0 (Zero.zero.{max u2 u1} (σ -> R) (Pi.instZero.{u2, u1} σ (fun (ᾰ : σ) => R) (fun (i : σ) => MulZeroClass.toHasZero.{u1} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)))))))))) (MvPolynomial.constantCoeff.{u1, u2} R σ _inst_1) but is expected to have type - forall {R : Type.{u2}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R], Eq.{max (succ u2) (succ u1)} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.eval.{u2, u1} R σ _inst_1 (OfNat.ofNat.{max u2 u1} (σ -> R) 0 (Zero.toOfNat0.{max u2 u1} (σ -> R) (Pi.instZero.{u1, u2} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20604 : σ) => R) (fun (i : σ) => CommMonoidWithZero.toZero.{u2} R (CommSemiring.toCommMonoidWithZero.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) + forall {R : Type.{u2}} {σ : Type.{u1}} [_inst_1 : CommSemiring.{u2} R], Eq.{max (succ u2) (succ u1)} (RingHom.{max u2 u1, u2} (MvPolynomial.{u1, u2} σ R _inst_1) R (Semiring.toNonAssocSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (CommSemiring.toSemiring.{max u2 u1} (MvPolynomial.{u1, u2} σ R _inst_1) (MvPolynomial.commSemiring.{u2, u1} R σ _inst_1))) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (MvPolynomial.eval.{u2, u1} R σ _inst_1 (OfNat.ofNat.{max u2 u1} (σ -> R) 0 (Zero.toOfNat0.{max u2 u1} (σ -> R) (Pi.instZero.{u1, u2} σ (fun (a._@.Mathlib.Data.MvPolynomial.Basic._hyg.20672 : σ) => R) (fun (i : σ) => CommMonoidWithZero.toZero.{u2} R (CommSemiring.toCommMonoidWithZero.{u2} R _inst_1)))))) (MvPolynomial.constantCoeff.{u2, u1} R σ _inst_1) Case conversion may be inaccurate. Consider using '#align mv_polynomial.eval_zero MvPolynomial.eval_zeroₓ'. -/ @[simp] theorem eval_zero : eval (0 : σ → R) = constantCoeff := diff --git a/Mathbin/Data/Nat/Multiplicity.lean b/Mathbin/Data/Nat/Multiplicity.lean index 131ba3b9b4..28897241bf 100644 --- a/Mathbin/Data/Nat/Multiplicity.lean +++ b/Mathbin/Data/Nat/Multiplicity.lean @@ -53,6 +53,12 @@ open BigOperators Nat namespace Nat +/- warning: nat.multiplicity_eq_card_pow_dvd -> Nat.multiplicity_eq_card_pow_dvd is a dubious translation: +lean 3 declaration is + forall {m : Nat} {n : Nat} {b : Nat}, (Ne.{1} Nat m (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) -> (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero))) n) -> (LT.lt.{0} Nat Nat.hasLt (Nat.log m n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) m n) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => Dvd.Dvd.{0} Nat Nat.hasDvd (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) m i) n) (fun (a : Nat) => Nat.decidableDvd (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) m a) n) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b))))) +but is expected to have type + forall {m : Nat} {n : Nat} {b : Nat}, (Ne.{1} Nat m (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) -> (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) n) -> (LT.lt.{0} Nat instLTNat (Nat.log m n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) m n) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => Dvd.dvd.{0} Nat Nat.instDvdNat (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) m i) n) (fun (a : Nat) => Nat.decidable_dvd (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) m a) n) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b))))) +Case conversion may be inaccurate. Consider using '#align nat.multiplicity_eq_card_pow_dvd Nat.multiplicity_eq_card_pow_dvdₓ'. -/ /-- The multiplicity of `m` in `n` is the number of positive natural numbers `i` such that `m ^ i` divides `n`. This set is expressed by filtering `Ico 1 b` where `b` is any bound greater than `log m n`. -/ @@ -80,28 +86,64 @@ theorem multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) ( namespace Prime +/- warning: nat.prime.multiplicity_one -> Nat.Prime.multiplicity_one is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) (OfNat.ofNat.{0} PartENat 0 (OfNat.mk.{0} PartENat 0 (Zero.zero.{0} PartENat PartENat.hasZero)))) +but is expected to have type + forall {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (OfNat.ofNat.{0} PartENat 0 (Zero.toOfNat0.{0} PartENat PartENat.instZeroPartENat))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_one Nat.Prime.multiplicity_oneₓ'. -/ theorem multiplicity_one {p : ℕ} (hp : p.Prime) : multiplicity p 1 = 0 := multiplicity.one_right hp.Prime.not_unit #align nat.prime.multiplicity_one Nat.Prime.multiplicity_one +/- warning: nat.prime.multiplicity_mul -> Nat.Prime.multiplicity_mul is a dubious translation: +lean 3 declaration is + forall {p : Nat} {m : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat Nat.hasMul) m n)) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p m) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p n))) +but is expected to have type + forall {p : Nat} {m : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) m n)) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p m) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p n))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_mul Nat.Prime.multiplicity_mulₓ'. -/ theorem multiplicity_mul {p m n : ℕ} (hp : p.Prime) : multiplicity p (m * n) = multiplicity p m + multiplicity p n := multiplicity.mul hp.Prime #align nat.prime.multiplicity_mul Nat.Prime.multiplicity_mul +/- warning: nat.prime.multiplicity_pow -> Nat.Prime.multiplicity_pow is a dubious translation: +lean 3 declaration is + forall {p : Nat} {m : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) m n)) (SMul.smul.{0, 0} Nat PartENat (AddMonoid.SMul.{0} PartENat (AddMonoidWithOne.toAddMonoid.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))) n (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p m))) +but is expected to have type + forall {p : Nat} {m : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) m n)) (HSMul.hSMul.{0, 0, 0} Nat PartENat PartENat (instHSMul.{0, 0} Nat PartENat (AddMonoid.SMul.{0} PartENat (AddMonoidWithOne.toAddMonoid.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)))) n (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p m))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_pow Nat.Prime.multiplicity_powₓ'. -/ theorem multiplicity_pow {p m n : ℕ} (hp : p.Prime) : multiplicity p (m ^ n) = n • multiplicity p m := multiplicity.pow hp.Prime #align nat.prime.multiplicity_pow Nat.Prime.multiplicity_pow +/- warning: nat.prime.multiplicity_self -> Nat.Prime.multiplicity_self is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p p) (OfNat.ofNat.{0} PartENat 1 (OfNat.mk.{0} PartENat 1 (One.one.{0} PartENat PartENat.hasOne)))) +but is expected to have type + forall {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p p) (OfNat.ofNat.{0} PartENat 1 (One.toOfNat1.{0} PartENat PartENat.instOnePartENat))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_self Nat.Prime.multiplicity_selfₓ'. -/ theorem multiplicity_self {p : ℕ} (hp : p.Prime) : multiplicity p p = 1 := multiplicity_self hp.Prime.not_unit hp.NeZero #align nat.prime.multiplicity_self Nat.Prime.multiplicity_self +/- warning: nat.prime.multiplicity_pow_self -> Nat.Prime.multiplicity_pow_self is a dubious translation: +lean 3 declaration is + forall {p : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) n)) +but is expected to have type + forall {p : Nat} {n : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) n)) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_pow_self Nat.Prime.multiplicity_pow_selfₓ'. -/ theorem multiplicity_pow_self {p n : ℕ} (hp : p.Prime) : multiplicity p (p ^ n) = n := multiplicity_pow_self hp.NeZero hp.Prime.not_unit n #align nat.prime.multiplicity_pow_self Nat.Prime.multiplicity_pow_self +/- warning: nat.prime.multiplicity_factorial -> Nat.Prime.multiplicity_factorial is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (Nat.Prime p) -> (forall {n : Nat} {b : Nat}, (LT.lt.{0} Nat Nat.hasLt (Nat.log p n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial n)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.hasDiv) n (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)))))) +but is expected to have type + forall {p : Nat}, (Nat.Prime p) -> (forall {n : Nat} {b : Nat}, (LT.lt.{0} Nat instLTNat (Nat.log p n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial n)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.instDivNat) n (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)))))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_factorial Nat.Prime.multiplicity_factorialₓ'. -/ /-- **Legendre's Theorem** The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed @@ -128,6 +170,12 @@ theorem multiplicity_factorial {p : ℕ} (hp : p.Prime) : #align nat.prime.multiplicity_factorial Nat.Prime.multiplicity_factorial +/- warning: nat.prime.multiplicity_factorial_mul_succ -> Nat.Prime.multiplicity_factorial_mul_succ is a dubious translation: +lean 3 declaration is + forall {n : Nat} {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat Nat.hasMul) p (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))))) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat Nat.hasMul) p n))) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) n (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))))) (OfNat.ofNat.{0} PartENat 1 (OfNat.mk.{0} PartENat 1 (One.one.{0} PartENat PartENat.hasOne))))) +but is expected to have type + forall {n : Nat} {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) p (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))))) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) p n))) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))))) (OfNat.ofNat.{0} PartENat 1 (One.toOfNat1.{0} PartENat PartENat.instOnePartENat)))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_factorial_mul_succ Nat.Prime.multiplicity_factorial_mul_succₓ'. -/ /-- The multiplicity of `p` in `(p * (n + 1))!` is one more than the sum of the multiplicities of `p` in `(p * n)!` and `n + 1`. -/ theorem multiplicity_factorial_mul_succ {n p : ℕ} (hp : p.Prime) : @@ -158,6 +206,12 @@ theorem multiplicity_factorial_mul_succ {n p : ℕ} (hp : p.Prime) : hp.multiplicity_self, sum_congr rfl h4, sum_const_zero, zero_add, add_comm (1 : PartENat)] #align nat.prime.multiplicity_factorial_mul_succ Nat.Prime.multiplicity_factorial_mul_succ +/- warning: nat.prime.multiplicity_factorial_mul -> Nat.Prime.multiplicity_factorial_mul is a dubious translation: +lean 3 declaration is + forall {n : Nat} {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat Nat.hasMul) p n))) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial n)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) n))) +but is expected to have type + forall {n : Nat} {p : Nat}, (Nat.Prime p) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial (HMul.hMul.{0, 0, 0} Nat Nat Nat (instHMul.{0} Nat instMulNat) p n))) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial n)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) n))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_factorial_mul Nat.Prime.multiplicity_factorial_mulₓ'. -/ /-- The multiplicity of `p` in `(p * n)!` is `n` more than that of `n!`. -/ theorem multiplicity_factorial_mul {n p : ℕ} (hp : p.Prime) : multiplicity p (p * n)! = multiplicity p n ! + n := @@ -170,13 +224,21 @@ theorem multiplicity_factorial_mul {n p : ℕ} (hp : p.Prime) : rw [add_comm, add_assoc] #align nat.prime.multiplicity_factorial_mul Nat.Prime.multiplicity_factorial_mul +#print Nat.Prime.pow_dvd_factorial_iff /- /-- A prime power divides `n!` iff it is at most the sum of the quotients `n / p ^ i`. This sum is expressed over the set `Ico 1 b` where `b` is any bound greater than `log p n` -/ theorem pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.Prime) (hbn : log p n < b) : p ^ r ∣ n ! ↔ r ≤ ∑ i in Ico 1 b, n / p ^ i := by rw [← PartENat.coe_le_coe, ← hp.multiplicity_factorial hbn, ← pow_dvd_iff_le_multiplicity] #align nat.prime.pow_dvd_factorial_iff Nat.Prime.pow_dvd_factorial_iff +-/ +/- warning: nat.prime.multiplicity_factorial_le_div_pred -> Nat.Prime.multiplicity_factorial_le_div_pred is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (Nat.Prime p) -> (forall (n : Nat), LE.le.{0} PartENat PartENat.hasLe (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.factorial n)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) (HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.hasDiv) n (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) p (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))))))) +but is expected to have type + forall {p : Nat}, (Nat.Prime p) -> (forall (n : Nat), LE.le.{0} PartENat PartENat.instLEPartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.factorial n)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) (HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.instDivNat) n (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) p (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_factorial_le_div_pred Nat.Prime.multiplicity_factorial_le_div_predₓ'. -/ theorem multiplicity_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) : multiplicity p n ! ≤ (n / (p - 1) : ℕ) := by @@ -184,6 +246,12 @@ theorem multiplicity_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) : exact Nat.geom_sum_Ico_le hp.two_le _ _ #align nat.prime.multiplicity_factorial_le_div_pred Nat.Prime.multiplicity_factorial_le_div_pred +/- warning: nat.prime.multiplicity_choose_aux -> Nat.Prime.multiplicity_choose_aux is a dubious translation: +lean 3 declaration is + forall {p : Nat} {n : Nat} {b : Nat} {k : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat Nat.hasLe k n) -> (Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.hasDiv) n (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i))) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.hasDiv) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i))) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.hasDiv) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)))) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => LE.le.{0} Nat Nat.hasLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)))) (fun (a : Nat) => Nat.decidableLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a)))) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b))))) +but is expected to have type + forall {p : Nat} {n : Nat} {b : Nat} {k : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat instLENat k n) -> (Eq.{1} Nat (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.instDivNat) n (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i))) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.instDivNat) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i))) (Finset.sum.{0, 0} Nat Nat Nat.addCommMonoid (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b) (fun (i : Nat) => HDiv.hDiv.{0, 0, 0} Nat Nat Nat (instHDiv.{0} Nat Nat.instDivNat) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)))) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => LE.le.{0} Nat instLENat (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)))) (fun (a : Nat) => Nat.decLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a)))) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b))))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_choose_aux Nat.Prime.multiplicity_choose_auxₓ'. -/ theorem multiplicity_choose_aux {p n b k : ℕ} (hp : p.Prime) (hkn : k ≤ n) : (∑ i in Finset.Ico 1 b, n / p ^ i) = ((∑ i in Finset.Ico 1 b, k / p ^ i) + ∑ i in Finset.Ico 1 b, (n - k) / p ^ i) + @@ -199,6 +267,12 @@ theorem multiplicity_choose_aux {p n b k : ℕ} (hp : p.Prime) (hkn : k ≤ n) : #align nat.prime.multiplicity_choose_aux Nat.Prime.multiplicity_choose_aux +/- warning: nat.prime.multiplicity_choose -> Nat.Prime.multiplicity_choose is a dubious translation: +lean 3 declaration is + forall {p : Nat} {n : Nat} {k : Nat} {b : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat Nat.hasLe k n) -> (LT.lt.{0} Nat Nat.hasLt (Nat.log p n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.choose n k)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => LE.le.{0} Nat Nat.hasLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p i)))) (fun (a : Nat) => Nat.decidableLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat Nat.hasAdd) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.hasMod) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p a)))) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring))) Nat.locallyFiniteOrder (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne))) b))))) +but is expected to have type + forall {p : Nat} {n : Nat} {k : Nat} {b : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat instLENat k n) -> (LT.lt.{0} Nat instLTNat (Nat.log p n) b) -> (Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.choose n k)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) (Finset.card.{0} Nat (Finset.filter.{0} Nat (fun (i : Nat) => LE.le.{0} Nat instLENat (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p i)))) (fun (a : Nat) => Nat.decLe (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a) (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a)) (HMod.hMod.{0, 0, 0} Nat Nat Nat (instHMod.{0} Nat Nat.instModNat) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n k) (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p a)))) (Finset.Ico.{0} Nat (PartialOrder.toPreorder.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring)) instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) b))))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_choose Nat.Prime.multiplicity_chooseₓ'. -/ /-- The multiplicity of `p` in `choose n k` is the number of carries when `k` and `n - k` are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b` is any bound greater than `log p n`. -/ @@ -223,6 +297,12 @@ theorem multiplicity_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb h₁ #align nat.prime.multiplicity_choose Nat.Prime.multiplicity_choose +/- warning: nat.prime.multiplicity_le_multiplicity_choose_add -> Nat.Prime.multiplicity_le_multiplicity_choose_add is a dubious translation: +lean 3 declaration is + forall {p : Nat}, (Nat.Prime p) -> (forall (n : Nat) (k : Nat), LE.le.{0} PartENat PartENat.hasLe (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p n) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.choose n k)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p k))) +but is expected to have type + forall {p : Nat}, (Nat.Prime p) -> (forall (n : Nat) (k : Nat), LE.le.{0} PartENat PartENat.instLEPartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p n) (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.choose n k)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p k))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_le_multiplicity_choose_add Nat.Prime.multiplicity_le_multiplicity_choose_addₓ'. -/ /-- A lower bound on the multiplicity of `p` in `choose n k`. -/ theorem multiplicity_le_multiplicity_choose_add {p : ℕ} (hp : p.Prime) : ∀ n k : ℕ, multiplicity p n ≤ multiplicity p (choose n k) + multiplicity p k @@ -237,6 +317,12 @@ theorem multiplicity_le_multiplicity_choose_add {p : ℕ} (hp : p.Prime) : variable {p n k : ℕ} +/- warning: nat.prime.multiplicity_choose_prime_pow_add_multiplicity -> Nat.Prime.multiplicity_choose_prime_pow_add_multiplicity is a dubious translation: +lean 3 declaration is + forall {p : Nat} {n : Nat} {k : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat Nat.hasLe k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n)) -> (Ne.{1} Nat k (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) -> (Eq.{1} PartENat (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.hasAdd) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.choose (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n) k)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p k)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) n)) +but is expected to have type + forall {p : Nat} {n : Nat} {k : Nat}, (Nat.Prime p) -> (LE.le.{0} Nat instLENat k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n)) -> (Ne.{1} Nat k (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> (Eq.{1} PartENat (HAdd.hAdd.{0, 0, 0} PartENat PartENat PartENat (instHAdd.{0} PartENat PartENat.instAddPartENat) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.choose (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n) k)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p k)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) n)) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_choose_prime_pow_add_multiplicity Nat.Prime.multiplicity_choose_prime_pow_add_multiplicityₓ'. -/ theorem multiplicity_choose_prime_pow_add_multiplicity (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : multiplicity p (choose (p ^ n) k) + multiplicity p k = n := le_antisymm @@ -257,6 +343,12 @@ theorem multiplicity_choose_prime_pow_add_multiplicity (hp : p.Prime) (hkn : k (by rw [← hp.multiplicity_pow_self] <;> exact multiplicity_le_multiplicity_choose_add hp _ _) #align nat.prime.multiplicity_choose_prime_pow_add_multiplicity Nat.Prime.multiplicity_choose_prime_pow_add_multiplicity +/- warning: nat.prime.multiplicity_choose_prime_pow -> Nat.Prime.multiplicity_choose_prime_pow is a dubious translation: +lean 3 declaration is + forall {p : Nat} {n : Nat} {k : Nat} (hp : Nat.Prime p), (LE.le.{0} Nat Nat.hasLe k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n)) -> (forall (hk0 : Ne.{1} Nat k (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))), Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p (Nat.choose (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat (Monoid.Pow.{0} Nat Nat.monoid)) p n) k)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat Nat.hasSub) n (Part.get.{0} Nat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) p k) (Iff.mpr (multiplicity.Finite.{0} Nat Nat.monoid p k) (And (Ne.{1} Nat p (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero))) k)) (multiplicity.finite_nat_iff p k) (And.intro (Ne.{1} Nat p (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))) (LT.lt.{0} Nat Nat.hasLt (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero))) k) (Nat.Prime.ne_one p hp) (Ne.bot_lt.{0} Nat (OrderedCancelAddCommMonoid.toPartialOrder.{0} Nat (StrictOrderedSemiring.toOrderedCancelAddCommMonoid.{0} Nat Nat.strictOrderedSemiring)) Nat.orderBot k hk0))))))) +but is expected to have type + forall {p : Nat} {n : Nat} {k : Nat} (hp : Nat.Prime p), (LE.le.{0} Nat instLENat k (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n)) -> (forall (hk0 : Ne.{1} Nat k (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))), Eq.{1} PartENat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p (Nat.choose (HPow.hPow.{0, 0, 0} Nat Nat Nat (instHPow.{0, 0} Nat Nat instPowNat) p n) k)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) (HSub.hSub.{0, 0, 0} Nat Nat Nat (instHSub.{0} Nat instSubNat) n (Part.get.{0} Nat (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) p k) (Iff.mpr (multiplicity.Finite.{0} Nat Nat.monoid p k) (And (Ne.{1} Nat p (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) k)) (multiplicity.finite_nat_iff p k) (And.intro (Ne.{1} Nat p (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (LT.lt.{0} Nat instLTNat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) k) (Nat.Prime.ne_one p hp) (Ne.bot_lt.{0} Nat (StrictOrderedSemiring.toPartialOrder.{0} Nat Nat.strictOrderedSemiring) Nat.orderBot k hk0))))))) +Case conversion may be inaccurate. Consider using '#align nat.prime.multiplicity_choose_prime_pow Nat.Prime.multiplicity_choose_prime_powₓ'. -/ theorem multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : multiplicity p (choose (p ^ n) k) = ↑(n - (multiplicity p k).get (finite_nat_iff.2 ⟨hp.ne_one, hk0.bot_lt⟩)) := @@ -264,6 +356,7 @@ theorem multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ multiplicity_choose_prime_pow_add_multiplicity hp hkn hk0 #align nat.prime.multiplicity_choose_prime_pow Nat.Prime.multiplicity_choose_prime_pow +#print Nat.Prime.dvd_choose_pow /- theorem dvd_choose_pow (hp : Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ (p ^ n).choose k := by obtain hkp | hkp := hkp.symm.lt_or_lt @@ -273,14 +366,23 @@ theorem dvd_choose_pow (hp : Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ rw [h, zero_add, eq_coe_iff] at H exact H.1 #align nat.prime.dvd_choose_pow Nat.Prime.dvd_choose_pow +-/ +#print Nat.Prime.dvd_choose_pow_iff /- theorem dvd_choose_pow_iff (hp : Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n := by refine' ⟨fun h => ⟨_, _⟩, fun h => dvd_choose_pow hp h.1 h.2⟩ <;> rintro rfl <;> simpa [hp.ne_one] using h #align nat.prime.dvd_choose_pow_iff Nat.Prime.dvd_choose_pow_iff +-/ end Prime +/- warning: nat.multiplicity_two_factorial_lt -> Nat.multiplicity_two_factorial_lt is a dubious translation: +lean 3 declaration is + forall {n : Nat}, (Ne.{1} Nat n (OfNat.ofNat.{0} Nat 0 (OfNat.mk.{0} Nat 0 (Zero.zero.{0} Nat Nat.hasZero)))) -> (LT.lt.{0} PartENat (Preorder.toLT.{0} PartENat (PartialOrder.toPreorder.{0} PartENat PartENat.partialOrder)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidableDvd a b) (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))) (Nat.factorial n)) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat PartENat (HasLiftT.mk.{1, 1} Nat PartENat (CoeTCₓ.coe.{1, 1} Nat PartENat (Nat.castCoe.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.addCommMonoidWithOne))))) n)) +but is expected to have type + forall {n : Nat}, (Ne.{1} Nat n (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> (LT.lt.{0} PartENat (Preorder.toLT.{0} PartENat (PartialOrder.toPreorder.{0} PartENat PartENat.partialOrder)) (multiplicity.{0} Nat Nat.monoid (fun (a : Nat) (b : Nat) => Nat.decidable_dvd a b) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (Nat.factorial n)) (Nat.cast.{0} PartENat (AddMonoidWithOne.toNatCast.{0} PartENat (AddCommMonoidWithOne.toAddMonoidWithOne.{0} PartENat PartENat.instAddCommMonoidWithOnePartENat)) n)) +Case conversion may be inaccurate. Consider using '#align nat.multiplicity_two_factorial_lt Nat.multiplicity_two_factorial_ltₓ'. -/ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (h : n ≠ 0), multiplicity 2 n ! < n := by have h2 := prime_two.prime diff --git a/Mathbin/Data/Zmod/Parity.lean b/Mathbin/Data/Zmod/Parity.lean index 6bd1bbaa91..74e0632d6e 100644 --- a/Mathbin/Data/Zmod/Parity.lean +++ b/Mathbin/Data/Zmod/Parity.lean @@ -24,16 +24,34 @@ parity, zmod, even, odd namespace ZMod +/- warning: zmod.eq_zero_iff_even -> ZMod.eq_zero_iff_even is a dubious translation: +lean 3 declaration is + forall {n : Nat}, Iff (Eq.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HasLiftT.mk.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (CoeTCₓ.coe.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Nat.castCoe.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddMonoidWithOne.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddGroupWithOne.toAddMonoidWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (NonAssocRing.toAddGroupWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (ZMod.field (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))) Nat.fact_prime_two)))))))))) n) (OfNat.ofNat.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 0 (OfNat.mk.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 0 (Zero.zero.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (MulZeroClass.toHasZero.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonUnitalNonAssocSemiring.toMulZeroClass.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonAssocRing.toNonUnitalNonAssocRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Ring.toNonAssocRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (DivisionRing.toRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Field.toDivisionRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (ZMod.field (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)) Nat.fact_prime_two)))))))))))) (Even.{0} Nat Nat.hasAdd n) +but is expected to have type + forall {n : Nat}, Iff (Eq.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Nat.cast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (NonAssocRing.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two))))) n) (OfNat.ofNat.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) 0 (Zero.toOfNat0.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (CommMonoidWithZero.toZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (CommGroupWithZero.toCommMonoidWithZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Semifield.toCommGroupWithZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toSemifield.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two)))))))) (Even.{0} Nat instAddNat n) +Case conversion may be inaccurate. Consider using '#align zmod.eq_zero_iff_even ZMod.eq_zero_iff_evenₓ'. -/ theorem eq_zero_iff_even {n : ℕ} : (n : ZMod 2) = 0 ↔ Even n := (CharP.cast_eq_zero_iff (ZMod 2) 2 n).trans even_iff_two_dvd.symm #align zmod.eq_zero_iff_even ZMod.eq_zero_iff_even +/- warning: zmod.eq_one_iff_odd -> ZMod.eq_one_iff_odd is a dubious translation: +lean 3 declaration is + forall {n : Nat}, Iff (Eq.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HasLiftT.mk.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (CoeTCₓ.coe.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Nat.castCoe.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddMonoidWithOne.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddGroupWithOne.toAddMonoidWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (NonAssocRing.toAddGroupWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (ZMod.field (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))) Nat.fact_prime_two)))))))))) n) (OfNat.ofNat.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 1 (OfNat.mk.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 1 (One.one.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (AddMonoidWithOne.toOne.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (AddGroupWithOne.toAddMonoidWithOne.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonAssocRing.toAddGroupWithOne.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Ring.toNonAssocRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (DivisionRing.toRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Field.toDivisionRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (ZMod.field (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)) Nat.fact_prime_two))))))))))) (Odd.{0} Nat Nat.semiring n) +but is expected to have type + forall {n : Nat}, Iff (Eq.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Nat.cast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (NonAssocRing.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two))))) n) (OfNat.ofNat.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) 1 (One.toOfNat1.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (NonAssocRing.toOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two)))))))) (Odd.{0} Nat Nat.semiring n) +Case conversion may be inaccurate. Consider using '#align zmod.eq_one_iff_odd ZMod.eq_one_iff_oddₓ'. -/ theorem eq_one_iff_odd {n : ℕ} : (n : ZMod 2) = 1 ↔ Odd n := by rw [← @Nat.cast_one (ZMod 2), ZMod.eq_iff_modEq_nat, Nat.odd_iff, Nat.ModEq] norm_num #align zmod.eq_one_iff_odd ZMod.eq_one_iff_odd +/- warning: zmod.ne_zero_iff_odd -> ZMod.ne_zero_iff_odd is a dubious translation: +lean 3 declaration is + forall {n : Nat}, Iff (Ne.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) ((fun (a : Type) (b : Type) [self : HasLiftT.{1, 1} a b] => self.0) Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (HasLiftT.mk.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (CoeTCₓ.coe.{1, 1} Nat (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Nat.castCoe.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddMonoidWithOne.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (AddGroupWithOne.toAddMonoidWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (NonAssocRing.toAddGroupWithOne.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))))) (ZMod.field (OfNat.ofNat.{0} Nat 2 (OfNat.mk.{0} Nat 2 (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)))) Nat.fact_prime_two)))))))))) n) (OfNat.ofNat.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 0 (OfNat.mk.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) 0 (Zero.zero.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (MulZeroClass.toHasZero.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonUnitalNonAssocSemiring.toMulZeroClass.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (NonAssocRing.toNonUnitalNonAssocRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Ring.toNonAssocRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (DivisionRing.toRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (Field.toDivisionRing.{0} (ZMod (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne))) (ZMod.field (bit0.{0} Nat Nat.hasAdd (One.one.{0} Nat Nat.hasOne)) Nat.fact_prime_two)))))))))))) (Odd.{0} Nat Nat.semiring n) +but is expected to have type + forall {n : Nat}, Iff (Ne.{1} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Nat.cast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (NonAssocRing.toNatCast.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Ring.toNonAssocRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (DivisionRing.toRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toDivisionRing.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two))))) n) (OfNat.ofNat.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) 0 (Zero.toOfNat0.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (CommMonoidWithZero.toZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (CommGroupWithZero.toCommMonoidWithZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Semifield.toCommGroupWithZero.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (Field.toSemifield.{0} (ZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (ZMod.instFieldZMod (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) Nat.fact_prime_two)))))))) (Odd.{0} Nat Nat.semiring n) +Case conversion may be inaccurate. Consider using '#align zmod.ne_zero_iff_odd ZMod.ne_zero_iff_oddₓ'. -/ theorem ne_zero_iff_odd {n : ℕ} : (n : ZMod 2) ≠ 0 ↔ Odd n := by constructor <;> · contrapose diff --git a/lake-manifest.json b/lake-manifest.json index eddc1c2c94..3bc4254af1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,15 +4,15 @@ [{"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "524083976fb4c37649900e830e228befd45a6e2d", + "rev": "e9f8c4b130145c0984e95a4e3ceaea90c87d87a5", "name": "lean3port", - "inputRev?": "524083976fb4c37649900e830e228befd45a6e2d"}}, + "inputRev?": "e9f8c4b130145c0984e95a4e3ceaea90c87d87a5"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "feb30eaeee8e45522fd4392a5ec87259a336d124", + "rev": "a86f11bb6623b0ffa089a4225f73ec406521c216", "name": "mathlib", - "inputRev?": "feb30eaeee8e45522fd4392a5ec87259a336d124"}}, + "inputRev?": "a86f11bb6623b0ffa089a4225f73ec406521c216"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 6c56c52cda..e9f6386223 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL System -- Usually the `tag` will be of the form `nightly-2021-11-22`. -- If you would like to use an artifact from a PR build, -- it will be of the form `pr-branchname-sha`. -def tag : String := "nightly-2023-03-19-14" +def tag : String := "nightly-2023-03-19-16" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"524083976fb4c37649900e830e228befd45a6e2d" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e9f8c4b130145c0984e95a4e3ceaea90c87d87a5" @[default_target] lean_lib Mathbin where