From 2cf5d19ea6332344026e0241473c0d2630da5d56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 18 Aug 2022 15:12:37 +0000 Subject: [PATCH] chore(algebra/*): Fix lint (#16128) Satisfy the `fintype_finite` and `to_additive_doc` linters. --- src/algebra/big_operators/fin.lean | 15 ++++++--------- src/algebra/big_operators/finprod.lean | 3 ++- src/algebra/big_operators/pi.lean | 10 +++++----- src/algebra/category/Group/limits.lean | 11 ++++++++--- src/algebra/char_p/basic.lean | 6 +++--- src/algebra/hom/freiman.lean | 7 ++++--- src/algebra/order/group.lean | 12 ++++++------ src/algebra/order/lattice_group.lean | 2 +- 8 files changed, 35 insertions(+), 31 deletions(-) diff --git a/src/algebra/big_operators/fin.lean b/src/algebra/big_operators/fin.lean index 6ecf74c21daaa..8645a7154fb64 100644 --- a/src/algebra/big_operators/fin.lean +++ b/src/algebra/big_operators/fin.lean @@ -58,27 +58,24 @@ theorem prod_univ_zero [comm_monoid β] (f : fin 0 → β) : ∏ i, f i = 1 := r /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the product of `f x`, for some `x : fin (n + 1)` times the remaining product -/ -@[to_additive -/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` -is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/] +@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of `f x`, +for some `x : fin (n + 1)` plus the remaining product"] theorem prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) : ∏ i, f i = f x * ∏ i : fin n, f (x.succ_above i) := by rw [univ_succ_above, prod_cons, finset.prod_map, rel_embedding.coe_fn_to_embedding] /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the product of `f 0` plus the remaining product -/ -@[to_additive -/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` -is the sum of `f 0` plus the remaining product -/] +@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of `f 0` +plus the remaining product"] theorem prod_univ_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) : ∏ i, f i = f 0 * ∏ i : fin n, f i.succ := prod_univ_succ_above f 0 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the product of `f (fin.last n)` plus the remaining product -/ -@[to_additive -/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` -is the sum of `f (fin.last n)` plus the remaining sum -/] +@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of +`f (fin.last n)` plus the remaining sum"] theorem prod_univ_cast_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) : ∏ i, f i = (∏ i : fin n, f i.cast_succ) * f (last n) := by simpa [mul_comm] using prod_univ_succ_above f (last n) diff --git a/src/algebra/big_operators/finprod.lean b/src/algebra/big_operators/finprod.lean index 2ff2a7280efac..b38c4c8b552f3 100644 --- a/src/algebra/big_operators/finprod.lean +++ b/src/algebra/big_operators/finprod.lean @@ -776,10 +776,11 @@ finprod_mem_mul_diff' hst (ht.inter_of_left _) @[to_additive "Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the sum of `f a` over the union `⋃ i, t i` is equal to the sum over all indexes `i` of the sums of `f a` over `a ∈ t i`."] -lemma finprod_mem_Union [fintype ι] {t : ι → set α} (h : pairwise (disjoint on t)) +lemma finprod_mem_Union [finite ι] {t : ι → set α} (h : pairwise (disjoint on t)) (ht : ∀ i, (t i).finite) : ∏ᶠ a ∈ (⋃ i : ι, t i), f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a := begin + casesI nonempty_fintype ι, lift t to ι → finset α using ht, classical, rw [← bUnion_univ, ← finset.coe_univ, ← finset.coe_bUnion, diff --git a/src/algebra/big_operators/pi.lean b/src/algebra/big_operators/pi.lean index dd4d4d6481263..25c49d9540b11 100644 --- a/src/algebra/big_operators/pi.lean +++ b/src/algebra/big_operators/pi.lean @@ -60,10 +60,10 @@ lemma finset.univ_sum_single [fintype I] (f : Π i, Z i) : ∑ i, pi.single i (f i) = f := by { ext a, simp } -lemma add_monoid_hom.functions_ext [fintype I] (G : Type*) - [add_comm_monoid G] (g h : (Π i, Z i) →+ G) - (w : ∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x)) : g = h := +lemma add_monoid_hom.functions_ext [finite I] (G : Type*) [add_comm_monoid G] + (g h : (Π i, Z i) →+ G) (w : ∀ i x, g (pi.single i x) = h (pi.single i x)) :g = h := begin + casesI nonempty_fintype I, ext k, rw [← finset.univ_sum_single k, g.map_sum, h.map_sum], simp only [w] @@ -72,7 +72,7 @@ end /-- This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in note [partially-applied ext lemmas]. -/ @[ext] -lemma add_monoid_hom.functions_ext' [fintype I] (M : Type*) [add_comm_monoid M] +lemma add_monoid_hom.functions_ext' [finite I] (M : Type*) [add_comm_monoid M] (g h : (Π i, Z i) →+ M) (H : ∀ i, g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) : g = h := @@ -86,7 +86,7 @@ open pi variables {I : Type*} [decidable_eq I] {f : I → Type*} variables [Π i, non_assoc_semiring (f i)] -@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [non_assoc_semiring G] +@[ext] lemma ring_hom.functions_ext [finite I] (G : Type*) [non_assoc_semiring G] (g h : (Π i, f i) →+* G) (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h := ring_hom.coe_add_monoid_hom_injective $ @add_monoid_hom.functions_ext I _ f _ _ G _ (g : (Π i, f i) →+ G) h w diff --git a/src/algebra/category/Group/limits.lean b/src/algebra/category/Group/limits.lean index 0878a696a834b..461221bd97900 100644 --- a/src/algebra/category/Group/limits.lean +++ b/src/algebra/category/Group/limits.lean @@ -66,7 +66,8 @@ the existing limit. -/ All we need to do is notice that the limit point has an `add_group` instance available, and then reuse the existing limit."] -instance (F : J ⥤ Group.{max v u}) : creates_limit F (forget₂ Group.{max v u} Mon.{max v u}) := +instance forget₂.creates_limit (F : J ⥤ Group.{max v u}) : + creates_limit F (forget₂ Group.{max v u} Mon.{max v u}) := creates_limit_of_reflects_iso (λ c' t, { lifted_cone := { X := Group.of (types.limit_cone (F ⋙ forget Group)).X, @@ -159,8 +160,12 @@ We show that the forgetful functor `CommGroup ⥤ Group` creates limits. All we need to do is notice that the limit point has a `comm_group` instance available, and then reuse the existing limit. -/ -@[to_additive] -instance (F : J ⥤ CommGroup.{max v u}) : creates_limit F (forget₂ CommGroup Group.{max v u}) := +@[to_additive "We show that the forgetful functor `AddCommGroup ⥤ AddGroup` creates limits. + +All we need to do is notice that the limit point has an `add_comm_group` instance available, and +then reuse the existing limit."] +instance forget₂.creates_limit (F : J ⥤ CommGroup.{max v u}) : + creates_limit F (forget₂ CommGroup Group.{max v u}) := creates_limit_of_reflects_iso (λ c' t, { lifted_cone := { X := CommGroup.of (types.limit_cone (F ⋙ forget CommGroup)).X, diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean index 46a92ff99b756..adaa870d5c620 100644 --- a/src/algebra/char_p/basic.lean +++ b/src/algebra/char_p/basic.lean @@ -329,10 +329,10 @@ theorem frobenius_inj [comm_ring R] [is_reduced R] /-- If `ring_char R = 2`, where `R` is a finite reduced commutative ring, then every `a : R` is a square. -/ -lemma is_square_of_char_two' {R : Type*} [fintype R] [comm_ring R] [is_reduced R] [char_p R 2] +lemma is_square_of_char_two' {R : Type*} [finite R] [comm_ring R] [is_reduced R] [char_p R 2] (a : R) : is_square a := -exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) $ - ((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a +by { casesI nonempty_fintype R, exact exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) + (((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a) } namespace char_p diff --git a/src/algebra/hom/freiman.lean b/src/algebra/hom/freiman.lean index 5de585bf795de..bc7ffa6628599 100644 --- a/src/algebra/hom/freiman.lean +++ b/src/algebra/hom/freiman.lean @@ -121,9 +121,10 @@ instance fun_like : fun_like (A →*[n] β) α (λ _, β) := instance freiman_hom_class : freiman_hom_class (A →*[n] β) A β n := { map_prod_eq_map_prod' := map_prod_eq_map_prod' } -/-- Helper instance for when there's too many metavariables to apply -`fun_like.has_coe_to_fun` directly. -/ -@[to_additive] +/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` +directly. -/ +@[to_additive "Helper instance for when there's too many metavariables to apply +`fun_like.has_coe_to_fun` directly."] instance : has_coe_to_fun (A →*[n] β) (λ _, α → β) := ⟨to_fun⟩ initialize_simps_projections freiman_hom (to_fun → apply) diff --git a/src/algebra/order/group.lean b/src/algebra/order/group.lean index 55a25bb9208bf..134ebffc95ddf 100644 --- a/src/algebra/order/group.lean +++ b/src/algebra/order/group.lean @@ -87,13 +87,13 @@ section typeclasses_left_le variables [has_le α] [covariant_class α α (*) (≤)] {a b c d : α} /-- Uses `left` co(ntra)variant. -/ -@[simp, to_additive left.neg_nonpos_iff] +@[simp, to_additive left.neg_nonpos_iff "Uses `left` co(ntra)variant."] lemma left.inv_le_one_iff : a⁻¹ ≤ 1 ↔ 1 ≤ a := by { rw [← mul_le_mul_iff_left a], simp } /-- Uses `left` co(ntra)variant. -/ -@[simp, to_additive left.nonneg_neg_iff] +@[simp, to_additive left.nonneg_neg_iff "Uses `left` co(ntra)variant."] lemma left.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1 := by { rw [← mul_le_mul_iff_left a], simp } @@ -128,13 +128,13 @@ section typeclasses_left_lt variables [has_lt α] [covariant_class α α (*) (<)] {a b c : α} /-- Uses `left` co(ntra)variant. -/ -@[simp, to_additive left.neg_pos_iff] +@[simp, to_additive left.neg_pos_iff "Uses `left` co(ntra)variant."] lemma left.one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1 := by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one] /-- Uses `left` co(ntra)variant. -/ -@[simp, to_additive left.neg_neg_iff] +@[simp, to_additive left.neg_neg_iff "Uses `left` co(ntra)variant."] lemma left.inv_lt_one_iff : a⁻¹ < 1 ↔ 1 < a := by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one] @@ -169,13 +169,13 @@ section typeclasses_right_le variables [has_le α] [covariant_class α α (swap (*)) (≤)] {a b c : α} /-- Uses `right` co(ntra)variant. -/ -@[simp, to_additive right.neg_nonpos_iff] +@[simp, to_additive right.neg_nonpos_iff "Uses `right` co(ntra)variant."] lemma right.inv_le_one_iff : a⁻¹ ≤ 1 ↔ 1 ≤ a := by { rw [← mul_le_mul_iff_right a], simp } /-- Uses `right` co(ntra)variant. -/ -@[simp, to_additive right.nonneg_neg_iff] +@[simp, to_additive right.nonneg_neg_iff "Uses `right` co(ntra)variant."] lemma right.one_le_inv_iff : 1 ≤ a⁻¹ ↔ a ≤ 1 := by { rw [← mul_le_mul_iff_right a], simp } diff --git a/src/algebra/order/lattice_group.lean b/src/algebra/order/lattice_group.lean index e90cb24f31213..4ddd79c0c4d14 100644 --- a/src/algebra/order/lattice_group.lean +++ b/src/algebra/order/lattice_group.lean @@ -471,7 +471,7 @@ sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c) /-- The absolute value satisfies the triangle inequality. -/ -@[to_additive abs_add_le] +@[to_additive abs_add_le "The absolute value satisfies the triangle inequality."] lemma mabs_mul_le [covariant_class α α (*) (≤)] (a b : α) : |a * b| ≤ |a| * |b| := begin apply sup_le,