bump to nightly-2023-03-19-08

mathlib commit leanprover-community/mathlib@1f4705c

Mathbin/Data/Polynomial/FieldDivision.lean

@@ -215,7 +215,7 @@ theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
 #align polynomial.div_by_monic_eq_div Polynomial.divByMonic_eq_div
 
 theorem mod_x_sub_c_eq_c_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=
-  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_x_sub_c_eq_c_eval _ _
+  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_X_sub_C_eq_C_eval _ _
 #align polynomial.mod_X_sub_C_eq_C_eval Polynomial.mod_x_sub_c_eq_c_eval
 
 theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=

Mathbin/RingTheory/Ideal/IdempotentFg.lean

@@ -18,6 +18,12 @@ import Mathbin.RingTheory.Finiteness
 
 namespace Ideal
 
+/- warning: ideal.is_idempotent_elem_iff_of_fg -> Ideal.isIdempotentElem_iff_of_fg is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : CommRing.{u1} R] (I : Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))), (Ideal.Fg.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) I) -> (Iff (IsIdempotentElem.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Ideal.hasMul.{u1} R (CommRing.toCommSemiring.{u1} R _inst_1)) I) (Exists.{succ u1} R (fun (e : R) => And (IsIdempotentElem.{u1} R (Distrib.toHasMul.{u1} R (Ring.toDistrib.{u1} R (CommRing.toRing.{u1} R _inst_1))) e) (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Submodule.span.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (Semiring.toModule.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Singleton.singleton.{u1, u1} R (Set.{u1} R) (Set.hasSingleton.{u1} R) e))))))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : CommRing.{u1} R] (I : Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))), (Ideal.Fg.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) I) -> (Iff (IsIdempotentElem.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Ideal.instMulIdealToSemiring.{u1} R (CommRing.toCommSemiring.{u1} R _inst_1)) I) (Exists.{succ u1} R (fun (e : R) => And (IsIdempotentElem.{u1} R (NonUnitalNonAssocRing.toMul.{u1} R (NonAssocRing.toNonUnitalNonAssocRing.{u1} R (Ring.toNonAssocRing.{u1} R (CommRing.toRing.{u1} R _inst_1)))) e) (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Submodule.span.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u1} R (NonAssocRing.toNonUnitalNonAssocRing.{u1} R (Ring.toNonAssocRing.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (_private.Mathlib.RingTheory.Ideal.Operations.0.Ideal.instModuleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonUnitalRingToNonUnitalCommRing.{u1, u1} R R (CommRing.toCommSemiring.{u1} R _inst_1) _inst_1 (Algebra.id.{u1} R (CommRing.toCommSemiring.{u1} R _inst_1))) (Singleton.singleton.{u1, u1} R (Set.{u1} R) (Set.instSingletonSet.{u1} R) e))))))
+Case conversion may be inaccurate. Consider using '#align ideal.is_idempotent_elem_iff_of_fg Ideal.isIdempotentElem_iff_of_fgₓ'. -/
 /-- A finitely generated idempotent ideal is generated by an idempotent element -/
 theorem isIdempotentElem_iff_of_fg {R : Type _} [CommRing R] (I : Ideal R) (h : I.Fg) :
     IsIdempotentElem I ↔ ∃ e : R, IsIdempotentElem e ∧ I = R ∙ e :=
@@ -38,6 +44,12 @@ theorem isIdempotentElem_iff_of_fg {R : Type _} [CommRing R] (I : Ideal R) (h :
     simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]
 #align ideal.is_idempotent_elem_iff_of_fg Ideal.isIdempotentElem_iff_of_fg
 
+/- warning: ideal.is_idempotent_elem_iff_eq_bot_or_top -> Ideal.isIdempotentElem_iff_eq_bot_or_top is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} [_inst_1 : CommRing.{u1} R] [_inst_2 : IsDomain.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))] (I : Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))), (Ideal.Fg.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) I) -> (Iff (IsIdempotentElem.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Ideal.hasMul.{u1} R (CommRing.toCommSemiring.{u1} R _inst_1)) I) (Or (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Bot.bot.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Submodule.hasBot.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (Semiring.toModule.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)))))) (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Top.top.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Submodule.hasTop.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (Semiring.toModule.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))))))
+but is expected to have type
+  forall {R : Type.{u1}} [_inst_1 : CommRing.{u1} R] [_inst_2 : IsDomain.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))] (I : Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))), (Ideal.Fg.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) I) -> (Iff (IsIdempotentElem.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Ideal.instMulIdealToSemiring.{u1} R (CommRing.toCommSemiring.{u1} R _inst_1)) I) (Or (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Bot.bot.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Submodule.instBotSubmodule.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (Semiring.toModule.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)))))) (Eq.{succ u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) I (Top.top.{u1} (Ideal.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))) (Submodule.instTopSubmodule.{u1, u1} R R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1)) (NonUnitalNonAssocSemiring.toAddCommMonoid.{u1} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))) (Semiring.toModule.{u1} R (Ring.toSemiring.{u1} R (CommRing.toRing.{u1} R _inst_1))))))))
+Case conversion may be inaccurate. Consider using '#align ideal.is_idempotent_elem_iff_eq_bot_or_top Ideal.isIdempotentElem_iff_eq_bot_or_topₓ'. -/
 theorem isIdempotentElem_iff_eq_bot_or_top {R : Type _} [CommRing R] [IsDomain R] (I : Ideal R)
     (h : I.Fg) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ :=
   by