bump to nightly-2023-03-04-12

mathlib commit leanprover-community/mathlib@62e8311
leanprover-community · Mar 4, 2023 · 726b2da · 726b2da
1 parent b1f9b87
commit 726b2da
Show file tree

Hide file tree

Showing 49 changed files with 2,044 additions and 763 deletions.
diff --git a/Mathbin/Algebra/Algebra/Equiv.lean b/Mathbin/Algebra/Algebra/Equiv.lean
diff --git a/Mathbin/Algebra/Algebra/Hom.lean b/Mathbin/Algebra/Algebra/Hom.lean
diff --git a/Mathbin/Algebra/BigOperators/Associated.lean b/Mathbin/Algebra/BigOperators/Associated.lean
@@ -258,7 +258,7 @@ theorem Prime.dvd_finset_prod_iff {S : Finset α} {p : M} (pp : Prime p) (g : α
 
 /- warning: prime.dvd_finsupp_prod_iff -> Prime.dvd_finsupp_prod_iff is a dubious translation:
 lean 3 declaration is
-  forall {α : Type.{u1}} {M : Type.{u2}} [_inst_1 : CommMonoidWithZero.{u2} M] {f : Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))} {g : α -> M -> Nat} {p : Nat}, (Prime.{0} Nat (LinearOrderedCommMonoidWithZero.toCommMonoidWithZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) p) -> (Iff (Dvd.Dvd.{0} Nat Nat.hasDvd p (Finsupp.prod.{u1, u2, 0} α M Nat (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) Nat.commMonoid f g)) (Exists.{succ u1} α (fun (a : α) => Exists.{0} (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a (Finsupp.support.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) f)) (fun (H : Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a (Finsupp.support.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) f)) => Dvd.Dvd.{0} Nat Nat.hasDvd p (g a (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) (fun (_x : Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) => α -> M) (Finsupp.hasCoeToFun.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) f a))))))
+  forall {α : Type.{u1}} {M : Type.{u2}} [_inst_1 : CommMonoidWithZero.{u2} M] {f : Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))} {g : α -> M -> Nat} {p : Nat}, (Prime.{0} Nat (LinearOrderedCommMonoidWithZero.toCommMonoidWithZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) p) -> (Iff (Dvd.Dvd.{0} Nat Nat.hasDvd p (Finsupp.prod.{u1, u2, 0} α M Nat (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) Nat.commMonoid f g)) (Exists.{succ u1} α (fun (a : α) => Exists.{0} (Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a (Finsupp.support.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) f)) (fun (H : Membership.Mem.{u1, u1} α (Finset.{u1} α) (Finset.hasMem.{u1} α) a (Finsupp.support.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1)))) f)) => Dvd.Dvd.{0} Nat Nat.hasDvd p (g a (coeFn.{max (succ u1) (succ u2), max (succ u1) (succ u2)} (Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) (fun (_x : Finsupp.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) => α -> M) (Finsupp.coeFun.{u1, u2} α M (MulZeroClass.toHasZero.{u2} M (MulZeroOneClass.toMulZeroClass.{u2} M (MonoidWithZero.toMulZeroOneClass.{u2} M (CommMonoidWithZero.toMonoidWithZero.{u2} M _inst_1))))) f a))))))
 but is expected to have type
   forall {α : Type.{u2}} {M : Type.{u1}} [_inst_1 : CommMonoidWithZero.{u1} M] {f : Finsupp.{u2, u1} α M (CommMonoidWithZero.toZero.{u1} M _inst_1)} {g : α -> M -> Nat} {p : Nat}, (Prime.{0} Nat (LinearOrderedCommMonoidWithZero.toCommMonoidWithZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) p) -> (Iff (Dvd.dvd.{0} Nat Nat.instDvdNat p (Finsupp.prod.{u2, u1, 0} α M Nat (CommMonoidWithZero.toZero.{u1} M _inst_1) Nat.commMonoid f g)) (Exists.{succ u2} α (fun (a : α) => And (Membership.mem.{u2, u2} α (Finset.{u2} α) (Finset.instMembershipFinset.{u2} α) a (Finsupp.support.{u2, u1} α M (CommMonoidWithZero.toZero.{u1} M _inst_1) f)) (Dvd.dvd.{0} Nat Nat.instDvdNat p (g a (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (Finsupp.{u2, u1} α M (CommMonoidWithZero.toZero.{u1} M _inst_1)) α (fun (a : α) => (fun (x._@.Mathlib.Data.Finsupp.Defs._hyg.779 : α) => M) a) (Finsupp.funLike.{u2, u1} α M (CommMonoidWithZero.toZero.{u1} M _inst_1)) f a))))))
 Case conversion may be inaccurate. Consider using '#align prime.dvd_finsupp_prod_iff Prime.dvd_finsupp_prod_iffₓ'. -/