Merge remote-tracking branch 'origin/master' into shuffle_nnrat

Author: YaelDillies

src/algebra/algebra/subalgebra/pointwise.lean

@@ -11,6 +11,9 @@ import ring_theory.adjoin.basic
 /-!
 # Pointwise actions on subalgebras.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `R'` acts on an `R`-algebra `A` (so that `R'` and `R` actions commute)
 then we get an `R'` action on the collection of `R`-subalgebras.
 -/

src/algebra/algebra/unitization.lean

@@ -11,6 +11,9 @@ import algebra.hom.non_unital_alg
 /-!
 # Unitization of a non-unital algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a non-unital `R`-algebra `A` (given via the type classes
 `[non_unital_ring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]`) we construct
 the minimal unital `R`-algebra containing `A` as an ideal. This object `algebra.unitization R A` is

src/algebra/char_p/exp_char.lean

@@ -9,6 +9,9 @@ import data.nat.prime
 /-!
 # Exponential characteristic
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the exponential characteristic and establishes a few basic results relating
 it to the (ordinary characteristic).
 The definition is stated for a semiring, but the actual results are for nontrivial rings

src/algebra/direct_sum/module.lean

@@ -9,6 +9,9 @@ import linear_algebra.dfinsupp
 /-!
 # Direct sum of modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The first part of the file provides constructors for direct sums of modules. It provides a
 construction of the direct sum using the universal property and proves its uniqueness
 (`direct_sum.to_module.unique`).

src/algebra/field/ulift.lean

@@ -9,6 +9,9 @@ import algebra.ring.ulift
 /-!
 # Field instances for `ulift`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines instances for field, semifield and related structures on `ulift` types.
 
 (Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)

src/algebra/monoid_algebra/degree.lean

@@ -8,6 +8,9 @@ import algebra.monoid_algebra.support
 /-!
 # Lemmas about the `sup` and `inf` of the support of `add_monoid_algebra`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## TODO
 The current plan is to state and prove lemmas about `finset.sup (finsupp.support f) D` with a
 "generic" degree/weight function `D` from the grading Type `A` to a somewhat ordered Type `B`.

src/algebra/monoid_algebra/no_zero_divisors.lean

@@ -8,6 +8,9 @@ import algebra.monoid_algebra.support
 /-!
 # Variations on non-zero divisors in `add_monoid_algebra`s
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file studies the interaction between typeclass assumptions on two Types `R` and `A` and
 whether `add_monoid_algebra R A` has non-zero zero-divisors.  For some background on related
 questions, see [Kaplansky's Conjectures](https://en.wikipedia.org/wiki/Kaplansky%27s_conjectures),

src/algebra/quadratic_discriminant.lean

@@ -25,6 +25,8 @@ This file defines the discriminant of a quadratic and gives the solution to a qu
 - `quadratic_ne_zero_of_discrim_ne_sq`: if the discriminant has no square root,
   then the corresponding quadratic has no root.
 - `discrim_le_zero`: if a quadratic is always non-negative, then its discriminant is non-positive.
+- `discrim_le_zero_of_nonpos`, `discrim_lt_zero`, `discrim_lt_zero_of_neg`: versions of this
+  statement with other inequalities.
 
 ## Tags
 
@@ -39,46 +41,47 @@ variables {R : Type*}
 /-- Discriminant of a quadratic -/
 def discrim [ring R] (a b c : R) : R := b^2 - 4 * a * c
 
-variables [comm_ring R] [is_domain R] {a b c : R}
+@[simp] lemma discrim_neg [ring R] (a b c : R) : discrim (-a) (-b) (-c) = discrim a b c :=
+by simp [discrim]
+
+variables [comm_ring R] {a b c : R}
+
+lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * x * x + b * x + c = 0) :
+  discrim a b c = (2 * a * x + b) ^ 2 :=
+begin
+  rw [discrim],
+  linear_combination -4 * a * h
+end
 
 /--
 A quadratic has roots if and only if its discriminant equals some square.
 -/
-lemma quadratic_eq_zero_iff_discrim_eq_sq (h2 : (2 : R) ≠ 0) (ha : a ≠ 0) (x : R) :
+lemma quadratic_eq_zero_iff_discrim_eq_sq [ne_zero (2 : R)] [no_zero_divisors R]
+  (ha : a ≠ 0) {x : R} :
   a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 :=
 begin
-  dsimp [discrim] at *,
-  split,
-  { assume h,
-    linear_combination -4 * a * h },
-  { assume h,
-    have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero h2 h2) ha,
-    apply mul_left_cancel₀ ha,
-    linear_combination -h }
+  refine ⟨discrim_eq_sq_of_quadratic_eq_zero, λ h, _⟩,
+  rw [discrim] at h,
+  have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (ne_zero.ne _) (ne_zero.ne _)) ha,
+  apply mul_left_cancel₀ ha,
+  linear_combination -h
 end
 
 /-- A quadratic has no root if its discriminant has no square root. -/
-lemma quadratic_ne_zero_of_discrim_ne_sq (h2 : (2 : R) ≠ 0) (ha : a ≠ 0)
-  (h : ∀ s : R, discrim a b c ≠ s * s) (x : R) :
+lemma quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s^2) (x : R) :
   a * x * x + b * x + c ≠ 0 :=
-begin
-  assume h',
-  rw [quadratic_eq_zero_iff_discrim_eq_sq h2 ha, sq] at h',
-  exact h _ h'
-end
+mt discrim_eq_sq_of_quadratic_eq_zero $ h _
 
 end ring
 
 section field
-variables {K : Type*} [field K] [invertible (2 : K)] {a b c x : K}
+variables {K : Type*} [field K] [ne_zero (2 : K)] {a b c x : K}
 
-/-- Roots of a quadratic -/
+/-- Roots of a quadratic equation. -/
 lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
   a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) :=
 begin
-  have h2 : (2 : K) ≠ 0 := nonzero_of_invertible 2,
-  rw [quadratic_eq_zero_iff_discrim_eq_sq h2 ha, h, sq, mul_self_eq_mul_self_iff],
-  have ne : 2 * a ≠ 0 := mul_ne_zero h2 ha,
+  rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff],
   field_simp,
   apply or_congr,
   { split; intro h'; linear_combination -h' },
@@ -108,7 +111,7 @@ end field
 section linear_ordered_field
 variables {K : Type*} [linear_ordered_field K] {a b c : K}
 
-/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
+/-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive. -/
 lemma discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a b c ≤ 0 :=
 begin
   rw [discrim, sq],
@@ -120,19 +123,20 @@ begin
     rcases (this.eventually (eventually_lt_at_bot 0)).exists with ⟨x, hx⟩,
     exact false.elim ((h x).not_lt $ by rwa ← add_mul) },
   -- if a = 0
-  { rcases em (b = 0) with (rfl|hb),
+  { rcases eq_or_ne b 0 with (rfl|hb),
     { simp },
     { have := h ((-c - 1) / b), rw [mul_div_cancel' _ hb] at this, linarith } },
   -- if a > 0
-  { have := calc
-      4 * a * (a * (-(b / a) * (1 / 2)) * (-(b / a) * (1 / 2)) + b * (-(b / a) * (1 / 2)) + c)
-          = (a * (b / a)) * (a * (b / a)) - 2 * (a * (b / a)) * b + 4 * a * c : by ring
-      ... = -(b * b - 4 * a * c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
-    have ha' : 0 ≤ 4 * a, by linarith,
-    have h := (mul_nonneg ha' (h (-(b / a) * (1 / 2)))),
-    rw this at h, rwa ← neg_nonneg }
+  { have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le,
+    have := h (-b / (2 * a)),
+    convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))),
+    field_simp [ha.ne'],
+    ring }
 end
 
+lemma discrim_le_zero_of_nonpos (h : ∀ x : K, a * x * x + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
+discrim_neg a b c ▸ discrim_le_zero (by simpa only [neg_mul, ← neg_add, neg_nonneg])
+
 /--
 If a polynomial of degree 2 is always positive, then its discriminant is negative,
 at least when the coefficient of the quadratic term is nonzero.
@@ -148,4 +152,8 @@ begin
   linarith
 end
 
+lemma discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * x * x + b * x + c < 0) :
+  discrim a b c < 0 :=
+discrim_neg a b c ▸ discrim_lt_zero (neg_ne_zero.2 ha) (by simpa only [neg_mul, ← neg_add, neg_pos])
+
 end linear_ordered_field

src/algebra/triv_sq_zero_ext.lean

@@ -10,6 +10,9 @@ import linear_algebra.prod
 /-!
 # Trivial Square-Zero Extension
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a ring `R` together with an `(R, R)`-bimodule `M`, the trivial square-zero extension of `M`
 over `R` is defined to be the `R`-algebra `R ⊕ M` with multiplication given by
 `(r₁ + m₁) * (r₂ + m₂) = r₁ r₂ + r₁ m₂ + m₁ r₂`.

src/category_theory/category/Bipointed.lean

@@ -8,6 +8,9 @@ import category_theory.category.Pointed
 /-!
 # The category of bipointed types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This defines `Bipointed`, the category of bipointed types.
 
 ## TODO