Merge remote-tracking branch 'origin/master' into graded_algebra_time…

…out'

src/algebra/direct_sum/internal.lean

@@ -47,6 +47,10 @@ instance add_comm_monoid.of_submonoid_on_semiring [semiring R] [set_like σ R]
   [add_submonoid_class σ R] (A : ι → σ) : ∀ i, add_comm_monoid (A i) :=
 λ i, by apply_instance
 
+instance add_comm_group.of_subgroup_on_semiring [ring R] [set_like σ R]
+  [add_subgroup_class σ R] (A : ι → σ) : ∀ i, add_comm_group (A i) :=
+λ i, by apply_instance
+
 lemma set_like.has_graded_one.algebra_map_mem [has_zero ι]
   [comm_semiring S] [semiring R] [algebra S R]
   (A : ι → submodule S R) [set_like.has_graded_one A] (s : S) : algebra_map S R s ∈ A 0 :=
@@ -55,6 +59,28 @@ begin
   exact ((A 0).smul_mem s set_like.has_graded_one.one_mem),
 end
 
+lemma set_like.has_graded_one.nat_cast_mem [has_zero ι] [add_monoid_with_one R]
+  [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.has_graded_one A] (n : ℕ) :
+  (n : R) ∈ A 0:=
+begin
+  induction n,
+  { rw nat.cast_zero,
+    exact zero_mem (A 0), },
+  { rw nat.cast_succ,
+    exact add_mem n_ih set_like.has_graded_one.one_mem, },
+end
+
+lemma set_like.has_graded_one.int_cast_mem [has_zero ι] [add_group_with_one R]
+  [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) [set_like.has_graded_one A] (z : ℤ) :
+  (z : R) ∈ A 0:=
+begin
+  induction z,
+  { rw int.cast_of_nat,
+    exact set_like.has_graded_one.nat_cast_mem _ _, },
+  { rw int.cast_neg_succ_of_nat,
+    exact neg_mem (set_like.has_graded_one.nat_cast_mem _ _), },
+end
+
 section direct_sum
 variables [decidable_eq ι]
 
@@ -81,6 +107,9 @@ instance gsemiring [add_monoid ι] [semiring R] [set_like σ R] [add_submonoid_c
   zero_mul := λ i j _, subtype.ext (zero_mul _),
   mul_add := λ i j _ _ _, subtype.ext (mul_add _ _ _),
   add_mul := λ i j _ _ _, subtype.ext (add_mul _ _ _),
+  nat_cast := λ n, ⟨n, set_like.has_graded_one.nat_cast_mem _ _⟩,
+  nat_cast_zero := subtype.ext nat.cast_zero,
+  nat_cast_succ := λ n, subtype.ext (nat.cast_succ n),
   ..set_like.gmonoid A }
 
 /-- Build a `gcomm_semiring` instance for a collection of additive submonoids. -/
@@ -90,6 +119,22 @@ instance gcomm_semiring [add_comm_monoid ι] [comm_semiring R] [set_like σ R]
 { ..set_like.gcomm_monoid A,
   ..set_like.gsemiring A, }
 
+/-- Build a `gring` instance for a collection of additive subgroups. -/
+instance gring [add_monoid ι] [ring R] [set_like σ R] [add_subgroup_class σ R]
+  (A : ι → σ) [set_like.graded_monoid A] :
+  direct_sum.gring (λ i, A i) :=
+{ int_cast := λ z, ⟨z, set_like.has_graded_one.int_cast_mem _ _⟩,
+  int_cast_of_nat := λ n, subtype.ext $ int.cast_of_nat _,
+  int_cast_neg_succ_of_nat := λ n, subtype.ext $ int.cast_neg_succ_of_nat n,
+  ..set_like.gsemiring A }
+
+/-- Build a `gcomm_semiring` instance for a collection of additive submonoids. -/
+instance gcomm_ring [add_comm_monoid ι] [comm_ring R] [set_like σ R]
+  [add_subgroup_class σ R] (A : ι → σ) [set_like.graded_monoid A] :
+  direct_sum.gcomm_ring (λ i, A i) :=
+{ ..set_like.gcomm_monoid A,
+  ..set_like.gring A, }
+
 end set_like
 
 /-- The canonical ring isomorphism between `⨁ i, A i` and `R`-/

src/algebra/direct_sum/ring.lean

@@ -17,26 +17,34 @@ additively-graded ring. The typeclasses are:
 
 * `direct_sum.gnon_unital_non_assoc_semiring A`
 * `direct_sum.gsemiring A`
+* `direct_sum.gring A`
 * `direct_sum.gcomm_semiring A`
+* `direct_sum.gcomm_ring A`
 
 Respectively, these imbue the external direct sum `⨁ i, A i` with:
 
 * `direct_sum.non_unital_non_assoc_semiring`, `direct_sum.non_unital_non_assoc_ring`
-* `direct_sum.semiring`, `direct_sum.ring`
-* `direct_sum.comm_semiring`, `direct_sum.comm_ring`
+* `direct_sum.semiring`
+* `direct_sum.ring`
+* `direct_sum.comm_semiring`
+* `direct_sum.comm_ring`
 
 the base ring `A 0` with:
 
 * `direct_sum.grade_zero.non_unital_non_assoc_semiring`,
   `direct_sum.grade_zero.non_unital_non_assoc_ring`
-* `direct_sum.grade_zero.semiring`, `direct_sum.grade_zero.ring`
-* `direct_sum.grade_zero.comm_semiring`, `direct_sum.grade_zero.comm_ring`
+* `direct_sum.grade_zero.semiring`
+* `direct_sum.grade_zero.ring`
+* `direct_sum.grade_zero.comm_semiring`
+* `direct_sum.grade_zero.comm_ring`
 
 and the `i`th grade `A i` with `A 0`-actions (`•`) defined as left-multiplication:
 
 * `direct_sum.grade_zero.has_scalar (A 0)`, `direct_sum.grade_zero.smul_with_zero (A 0)`
 * `direct_sum.grade_zero.module (A 0)`
 * (nothing)
+* (nothing)
+* (nothing)
 
 Note that in the presence of these instances, `⨁ i, A i` itself inherits an `A 0`-action.
 
@@ -95,12 +103,25 @@ variables (A : ι → Type*)
 
 /-- A graded version of `semiring`. -/
 class gsemiring [add_monoid ι] [Π i, add_comm_monoid (A i)] extends
-  gnon_unital_non_assoc_semiring A, graded_monoid.gmonoid A
+  gnon_unital_non_assoc_semiring A, graded_monoid.gmonoid A :=
+(nat_cast : ℕ → A 0)
+(nat_cast_zero : nat_cast 0 = 0)
+(nat_cast_succ : ∀ n : ℕ, nat_cast (n + 1) = nat_cast n + graded_monoid.ghas_one.one)
 
 /-- A graded version of `comm_semiring`. -/
 class gcomm_semiring [add_comm_monoid ι] [Π i, add_comm_monoid (A i)] extends
   gsemiring A, graded_monoid.gcomm_monoid A
 
+/-- A graded version of `ring`. -/
+class gring [add_monoid ι] [Π i, add_comm_group (A i)] extends gsemiring A :=
+(int_cast : ℤ → A 0)
+(int_cast_of_nat : ∀ n : ℕ, int_cast n = nat_cast n)
+(int_cast_neg_succ_of_nat : ∀ n : ℕ, int_cast (-(n+1 : ℕ)) = -nat_cast (n+1 : ℕ))
+
+/-- A graded version of `comm_ring`. -/
+class gcomm_ring [add_comm_monoid ι] [Π i, add_comm_group (A i)] extends
+  gring A, gcomm_semiring A
+
 end defs
 
 lemma of_eq_of_graded_monoid_eq {A : ι → Type*} [Π (i : ι), add_comm_monoid (A i)]
@@ -214,7 +235,9 @@ instance semiring : semiring (⨁ i, A i) :=
   one_mul := one_mul A,
   mul_one := mul_one A,
   mul_assoc := mul_assoc A,
-  ..add_monoid_with_one.unary,
+  nat_cast := λ n, of _ _ (gsemiring.nat_cast n),
+  nat_cast_zero := by rw [gsemiring.nat_cast_zero, map_zero],
+  nat_cast_succ := λ n, by { rw [gsemiring.nat_cast_succ, map_add], refl },
   ..direct_sum.non_unital_non_assoc_semiring _, }
 
 lemma of_pow {i} (a : A i) (n : ℕ) :
@@ -299,7 +322,7 @@ instance non_assoc_ring : non_unital_non_assoc_ring (⨁ i, A i) :=
 end non_unital_non_assoc_ring
 
 section ring
-variables [Π i, add_comm_group (A i)] [add_monoid ι] [gsemiring A]
+variables [Π i, add_comm_group (A i)] [add_monoid ι] [gring A]
 
 /-- The `ring` derived from `gsemiring A`. -/
 instance ring : ring (⨁ i, A i) :=
@@ -308,14 +331,17 @@ instance ring : ring (⨁ i, A i) :=
   zero := 0,
   add := (+),
   neg := has_neg.neg,
+  int_cast := λ z, of _ _ (gring.int_cast z),
+  int_cast_of_nat := λ z, congr_arg _ $ gring.int_cast_of_nat _,
+  int_cast_neg_succ_of_nat := λ z,
+    (congr_arg _ $ gring.int_cast_neg_succ_of_nat _).trans (map_neg _ _),
   ..(direct_sum.semiring _),
   ..(direct_sum.add_comm_group _), }
 
-
 end ring
 
 section comm_ring
-variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_semiring A]
+variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_ring A]
 
 /-- The `comm_ring` derived from `gcomm_semiring A`. -/
 instance comm_ring : comm_ring (⨁ i, A i) :=
@@ -373,12 +399,10 @@ variables [Π i, add_comm_monoid (A i)] [add_monoid ι] [gsemiring A]
 | 0 := by rw [pow_zero, pow_zero, direct_sum.of_zero_one]
 | (n + 1) := by rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow]
 
-instance : has_nat_cast (A 0) := ⟨nat.unary_cast⟩
+instance : has_nat_cast (A 0) := ⟨gsemiring.nat_cast⟩
 
 @[simp] lemma of_nat_cast (n : ℕ) : of A 0 n = n :=
-by induction n; simp [(of A 0).map_zero, (of A 0).map_add, *,
-  show ((0 : ℕ) : A 0) = 0, from rfl,
-  λ n : ℕ, show (n.succ : A 0) = (n : A 0) + 1, from rfl]
+rfl
 
 /-- The `semiring` structure derived from `gsemiring A`. -/
 instance grade_zero.semiring : semiring (A 0) :=
@@ -433,12 +457,12 @@ function.injective.non_unital_non_assoc_ring (of A 0) dfinsupp.single_injective
 end ring
 
 section ring
-variables [Π i, add_comm_group (A i)] [add_monoid ι] [gsemiring A]
+variables [Π i, add_comm_group (A i)] [add_monoid ι] [gring A]
 
-instance : has_int_cast (A 0) := ⟨int.cast_def⟩
+instance : has_int_cast (A 0) := ⟨gring.int_cast⟩
 
 @[simp] lemma of_int_cast (n : ℤ) : of A 0 n = n :=
-show of A 0 n.cast_def = n, by cases n; simp [int.cast_def]
+rfl
 
 /-- The `ring` derived from `gsemiring A`. -/
 instance grade_zero.ring : ring (A 0) :=
@@ -458,7 +482,7 @@ function.injective.ring (of A 0) dfinsupp.single_injective
 end ring
 
 section comm_ring
-variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_semiring A]
+variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_ring A]
 
 /-- The `comm_ring` derived from `gcomm_semiring A`. -/
 instance grade_zero.comm_ring : comm_ring (A 0) :=
@@ -588,7 +612,11 @@ instance non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring
 /-- A direct sum of copies of a `semiring` inherits the multiplication structure. -/
 instance semiring.direct_sum_gsemiring {R : Type*} [add_monoid ι] [semiring R] :
   direct_sum.gsemiring (λ i : ι, R) :=
-{ ..non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring ι, ..monoid.gmonoid ι }
+{ nat_cast := λ n, n,
+  nat_cast_zero := nat.cast_zero,
+  nat_cast_succ := nat.cast_succ,
+  ..non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring ι,
+  ..monoid.gmonoid ι }
 
 open_locale direct_sum
 

src/algebra/group/units.lean

@@ -415,6 +415,9 @@ begin
   simp [h.unit_spec]
 end
 
+/-- `is_unit x` is decidable if we can decide if `x` comes from `Mˣ`. -/
+instance [monoid M] (x : M) [h : decidable (∃ u : Mˣ, ↑u = x)] : decidable (is_unit x) := h
+
 section monoid
 variables [monoid M] {a b c : M}
 

src/algebra/order/ring.lean

@@ -1225,6 +1225,14 @@ begin
     exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩ }
 end
 
+@[simp] lemma max_zero_add_max_neg_zero_eq_abs_self (a : α) :
+  max a 0 + max (-a) 0 = |a| :=
+begin
+  symmetry,
+  rcases le_total 0 a with ha|ha;
+  simp [ha],
+end
+
 lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
 have nhc : 0 ≤ -c, from neg_nonneg_of_nonpos hc,
 have h2 : -(c * b) < -(c * a), from neg_lt_neg h,

src/combinatorics/simple_graph/clique.lean

@@ -142,6 +142,32 @@ forall_imp $ λ s, mt $ is_n_clique.mono h
 
 end clique_free
 
+/-! ### Set of cliques -/
+
+section clique_set
+variables (G) {n : ℕ} {a b c : α} {s : finset α}
+
+/-- The `n`-cliques in a graph as a set. -/
+def clique_set (n : ℕ) : set (finset α) := {s | G.is_n_clique n s}
+
+lemma mem_clique_set_iff : s ∈ G.clique_set n ↔ G.is_n_clique n s := iff.rfl
+
+@[simp] lemma clique_set_eq_empty_iff : G.clique_set n = ∅ ↔ G.clique_free n :=
+by simp_rw [clique_free, set.eq_empty_iff_forall_not_mem, mem_clique_set_iff]
+
+alias clique_set_eq_empty_iff ↔ _ simple_graph.clique_free.clique_set
+
+attribute [protected] clique_free.clique_set
+
+variables {G H}
+
+@[mono] lemma clique_set_mono (h : G ≤ H) : G.clique_set n ⊆ H.clique_set n :=
+λ _, is_n_clique.mono h
+
+lemma clique_set_mono' (h : G ≤ H) : G.clique_set ≤ H.clique_set := λ _, clique_set_mono h
+
+end clique_set
+
 /-! ### Finset of cliques -/
 
 section clique_finset
@@ -150,9 +176,12 @@ variables (G) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} {a
 /-- The `n`-cliques in a graph as a finset. -/
 def clique_finset (n : ℕ) : finset (finset α) := univ.filter $ G.is_n_clique n
 
-lemma mem_clique_finset_iff (s : finset α) : s ∈ G.clique_finset n ↔ G.is_n_clique n s :=
+lemma mem_clique_finset_iff : s ∈ G.clique_finset n ↔ G.is_n_clique n s :=
 mem_filter.trans $ and_iff_right $ mem_univ _
 
+@[simp] lemma coe_clique_finset (n : ℕ) : (G.clique_finset n : set (finset α)) = G.clique_set n :=
+set.ext $ λ _, mem_clique_finset_iff _
+
 @[simp] lemma clique_finset_eq_empty_iff : G.clique_finset n = ∅ ↔ G.clique_free n :=
 by simp_rw [clique_free, eq_empty_iff_forall_not_mem, mem_clique_finset_iff]
 
@@ -162,7 +191,7 @@ attribute [protected] clique_free.clique_finset
 
 variables {G} [decidable_rel H.adj]
 
-lemma clique_finset_mono (h : G ≤ H) : G.clique_finset n ⊆ H.clique_finset n :=
+@[mono] lemma clique_finset_mono (h : G ≤ H) : G.clique_finset n ⊆ H.clique_finset n :=
 monotone_filter_right _ $ λ _, is_n_clique.mono h
 
 end clique_finset

src/data/W/cardinal.lean

@@ -58,26 +58,20 @@ lemma cardinal_mk_le_max_aleph_0_of_fintype [Π a, fintype (β a)] : #(W_type β
     rw [cardinal.mk_eq_zero (W_type β)],
     exact zero_le _
   end) $
-λ hn,
-let m := max (#α) ℵ₀ in
-cardinal_mk_le_of_le $
-calc cardinal.sum (λ a : α, m ^ #(β a))
-    ≤ #α * cardinal.sup.{u u}
-      (λ a : α, m ^ cardinal.mk (β a)) :
-  cardinal.sum_le_sup _
-... ≤ m * cardinal.sup.{u u}
-      (λ a : α, m ^ #(β a)) :
-  mul_le_mul' (le_max_left _ _) le_rfl
+λ hn, let m := max (#α) ℵ₀ in cardinal_mk_le_of_le $
+calc cardinal.sum (λ a, m ^ #(β a))
+    ≤ #α * ⨆ a, m ^ #(β a) : cardinal.sum_le_supr _
+... ≤ m * ⨆ a, m ^ #(β a) : mul_le_mul' (le_max_left _ _) le_rfl
 ... = m : mul_eq_left.{u} (le_max_right _ _)
-  (cardinal.sup_le (λ i, pow_le (le_max_right _ _) (lt_aleph_0_of_fintype _)))
-  (pos_iff_ne_zero.1 (order.succ_le_iff.1
+  (csupr_le' $ λ i, pow_le (le_max_right _ _) (lt_aleph_0_of_fintype _)) $
+  pos_iff_ne_zero.1 $ order.succ_le_iff.1
     begin
-      rw [succ_zero],
+      rw succ_zero,
       obtain ⟨a⟩ : nonempty α, from hn,
-      refine le_trans _ (le_sup _ a),
-      rw [← @power_zero m],
+      refine le_trans _ (le_csupr (bdd_above_range.{u u} _) a),
+      rw ←power_zero,
       exact power_le_power_left (pos_iff_ne_zero.1
-        (lt_of_lt_of_le aleph_0_pos (le_max_right _ _))) (zero_le _)
-    end))
+        (aleph_0_pos.trans_le (le_max_right _ _))) (zero_le _)
+    end
 
 end W_type

src/data/nat/totient.lean

@@ -329,4 +329,29 @@ begin
   rw [sub_mul, one_mul, mul_comm, mul_inv_cancel hp', cast_pred hp],
 end
 
+lemma totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ a * φ b * (a.gcd b) :=
+begin
+  have shuffle : ∀ a1 a2 b1 b2 c1 c2 : ℕ, b1 ∣ a1 → b2 ∣ a2 →
+    (a1/b1 * c1) * (a2/b2 * c2) = (a1*a2)/(b1*b2) * (c1*c2),
+  { intros a1 a2 b1 b2 c1 c2 h1 h2,
+    calc
+      (a1/b1 * c1) * (a2/b2 * c2) = ((a1/b1) * (a2/b2)) * (c1*c2) : by apply mul_mul_mul_comm
+      ... = (a1*a2)/(b1*b2) * (c1*c2) : by { congr' 1, exact div_mul_div_comm h1 h2 } },
+  simp only [totient_eq_div_factors_mul],
+  rw [shuffle, shuffle],
+  rotate, repeat { apply prod_prime_factors_dvd },
+  { simp only [prod_factors_gcd_mul_prod_factors_mul],
+    rw [eq_comm, mul_comm, ←mul_assoc, ←nat.mul_div_assoc],
+    exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b) }
+end
+
+lemma totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) :=
+begin
+  let d := a.gcd b,
+  rcases (zero_le a).eq_or_lt with rfl | ha0, { simp },
+  have hd0 : 0 < d, from nat.gcd_pos_of_pos_left _ ha0,
+  rw [←mul_le_mul_right hd0, ←totient_gcd_mul_totient_mul a b, mul_comm],
+  apply mul_le_mul_left' (nat.totient_le d),
+end
+
 end nat