Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f1944b3

Browse files
YaelDilliesYaelDillies
committed
refactor(*): Extend ×ˢ notation (#15717)
Delete `has_set_prod` in favor of a direct notation declaration. Overload that notation with the `list`, `finset`, `multiset` versions. Use the new notation and remove type ascriptions to the existing uses where possible (because Lean gets more information from the notation now).
1 parent 24a55a0 commit f1944b3

72 files changed

Lines changed: 247 additions & 296 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎archive/100-theorems-list/73_ascending_descending_sequences.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ begin
132132
by_contra q,
133133
push_neg at q,
134134
-- Then the labels `(a_i, b_i)` all fit in the following set: `{ (x,y) | 1 ≤ x ≤ r, 1 ≤ y ≤ s }`
135-
let ran : finset (ℕ × ℕ) := ((range r).image nat.succ).product ((range s).image nat.succ),
135+
let ran : finset (ℕ × ℕ) := (range r).image nat.succ ×ˢ (range s).image nat.succ,
136136
-- which we prove here.
137137
have : image ab univ ⊆ ran,
138138
-- First some logical shuffling

‎archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ lemma card_le_two_pow_mul_sqrt {x k : ℕ} : card (M x k) ≤ 2 ^ k * nat.sqrt x
171171
begin
172172
let M₁ := {e ∈ M x k | squarefree (e + 1)},
173173
let M₂ := M (nat.sqrt x) k,
174-
let K := finset.product M₁ M₂,
174+
let K := M₁ ×ˢ M₂,
175175
let f : ℕ × ℕ → ℕ := λ mn, (mn.2 + 1) ^ 2 * (mn.1 + 1) - 1,
176176

177177
-- Every element of `M x k` is one less than the product `(m + 1)² * (r + 1)` with `r + 1`

‎src/algebra/algebra/subalgebra/basic.lean‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -810,12 +810,11 @@ variables (S₁ : subalgebra R B)
810810

811811
/-- The product of two subalgebras is a subalgebra. -/
812812
def prod : subalgebra R (A × B) :=
813-
{ carrier := (S : set A) ×ˢ (S₁ : set B),
813+
{ carrier := S ×ˢ S₁,
814814
algebra_map_mem' := λ r, ⟨algebra_map_mem _ _, algebra_map_mem _ _⟩,
815815
.. S.to_subsemiring.prod S₁.to_subsemiring }
816816

817-
@[simp] lemma coe_prod :
818-
(prod S S₁ : set (A × B)) = (S : set A) ×ˢ (S₁ : set B):= rfl
817+
@[simp] lemma coe_prod : (prod S S₁ : set (A × B)) = S ×ˢ S₁ := rfl
819818

820819
lemma prod_to_submodule :
821820
(S.prod S₁).to_submodule = S.to_submodule.prod S₁.to_submodule := rfl

‎src/algebra/big_operators/basic.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -512,24 +512,24 @@ eq.trans (by rw one_mul; refl) fold_op_distrib
512512

513513
@[to_additive]
514514
lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} :
515-
(∏ x in s.product t, f x) = ∏ x in s, ∏ y in t, f (x, y) :=
516-
prod_finset_product (s.product t) s (λ a, t) (λ p, mem_product)
515+
(∏ x in s ×ˢ t, f x) = ∏ x in s, ∏ y in t, f (x, y) :=
516+
prod_finset_product (s ×ˢ t) s (λ a, t) (λ p, mem_product)
517517

518518
/-- An uncurried version of `finset.prod_product`. -/
519519
@[to_additive "An uncurried version of `finset.sum_product`"]
520520
lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} :
521-
(∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
521+
(∏ x in s ×ˢ t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
522522
prod_product
523523

524524
@[to_additive]
525525
lemma prod_product_right {s : finset γ} {t : finset α} {f : γ×α → β} :
526-
(∏ x in s.product t, f x) = ∏ y in t, ∏ x in s, f (x, y) :=
527-
prod_finset_product_right (s.product t) t (λ a, s) (λ p, mem_product.trans and.comm)
526+
(∏ x in s ×ˢ t, f x) = ∏ y in t, ∏ x in s, f (x, y) :=
527+
prod_finset_product_right (s ×ˢ t) t (λ a, s) (λ p, mem_product.trans and.comm)
528528

529529
/-- An uncurried version of `finset.prod_product_right`. -/
530530
@[to_additive "An uncurried version of `finset.prod_product_right`"]
531531
lemma prod_product_right' {s : finset γ} {t : finset α} {f : γ → α → β} :
532-
(∏ x in s.product t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y :=
532+
(∏ x in s ×ˢ t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y :=
533533
prod_product_right
534534

535535
/-- Generalization of `finset.prod_comm` to the case when the inner `finset`s depend on the outer

‎src/algebra/big_operators/ring.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ add_monoid_hom.map_sum (add_monoid_hom.mul_left b) _ s
5252

5353
lemma sum_mul_sum {ι₁ : Type*} {ι₂ : Type*} (s₁ : finset ι₁) (s₂ : finset ι₂)
5454
(f₁ : ι₁ → β) (f₂ : ι₂ → β) :
55-
(∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁.product s₂, f₁ p.1 * f₂ p.2 :=
55+
(∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁ ×ˢ s₂, f₁ p.1 * f₂ p.2 :=
5656
by { rw [sum_product, sum_mul, sum_congr rfl], intros, rw mul_sum }
5757

5858
end semiring

‎src/algebra/direct_sum/internal.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,8 +152,7 @@ lemma direct_sum.coe_mul_apply [add_monoid ι] [semiring R] [set_like σ R]
152152
[add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A]
153153
[Π (i : ι) (x : A i), decidable (x ≠ 0)] (r r' : ⨁ i, A i) (i : ι) :
154154
((r * r') i : R) =
155-
∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
156-
r ij.1 * r' ij.2 :=
155+
∑ ij in (r.support ×ˢ r'.support).filter (λ ij : ι × ι, ij.1 + ij.2 = i), r ij.1 * r' ij.2 :=
157156
begin
158157
rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
159158
add_submonoid_class.coe_finset_sum],

‎src/algebra/direct_sum/ring.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,7 @@ open_locale big_operators
269269
lemma mul_eq_sum_support_ghas_mul
270270
[Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
271271
a * a' =
272-
∑ (ij : ι × ι) in (dfinsupp.support a).product (dfinsupp.support a'),
272+
∑ ij in dfinsupp.support a ×ˢ dfinsupp.support a',
273273
direct_sum.of _ _ (graded_monoid.ghas_mul.mul (a ij.fst) (a' ij.snd)) :=
274274
begin
275275
change direct_sum.mul_hom _ a a' = _,

‎src/algebra/indicator_function.lean‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -457,12 +457,8 @@ lemma inter_indicator_one {s t : set α} :
457457
funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply, one_mul])
458458

459459
lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} :
460-
(s ×ˢ t : set _).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
461-
begin
462-
letI := classical.dec_pred (∈ s),
463-
letI := classical.dec_pred (∈ t),
464-
simp [indicator_apply, ← ite_and],
465-
end
460+
(s ×ˢ t).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
461+
by { classical, simp [indicator_apply, ←ite_and] }
466462

467463
variables (M) [nontrivial M]
468464

‎src/algebra/monoid_algebra/basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -325,8 +325,8 @@ lemma mul_apply_antidiagonal [has_mul G] (f g : monoid_algebra k G) (x : G) (s :
325325
let F : G × G → k := λ p, by classical; exact if p.1 * p.2 = x then f p.1 * g p.2 else 0 in
326326
calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂)) :
327327
mul_apply f g x
328-
... = ∑ p in f.support.product g.support, F p : finset.sum_product.symm
329-
... = ∑ p in (f.support.product g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 :
328+
... = ∑ p in f.support ×ˢ g.support, F p : finset.sum_product.symm
329+
... = ∑ p in (f.support ×ˢ g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 :
330330
(finset.sum_filter _ _).symm
331331
... = ∑ p in s.filter (λ p : G × G, p.1 ∈ f.support ∧ p.2 ∈ g.support), f p.1 * g p.2 :
332332
sum_congr (by { ext, simp only [mem_filter, mem_product, hs, and_comm] }) (λ _ _, rfl)

‎src/algebraic_geometry/structure_sheaf.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -688,7 +688,7 @@ begin
688688
have n_spec := λ (p : ι × ι), (exists_power p.fst p.snd).some_spec,
689689
-- We need one power `(h i * h j) ^ N` that works for *all* pairs `(i,j)`
690690
-- Since there are only finitely many indices involved, we can pick the supremum.
691-
let N := (t.product t).sup n,
691+
let N := (t ×ˢ t).sup n,
692692
have basic_opens_eq : ∀ i : ι, basic_open ((h i) ^ (N+1)) = basic_open (h i) :=
693693
λ i, basic_open_pow _ _ (by linarith),
694694
-- Expanding the fraction `a i / h i` by the power `(h i) ^ N` gives the desired normalization

0 commit comments

Comments
 (0)