Skip to content

Commit 8c70e6d

Browse files
BoltonBaileyBoltonBailey
committed
new imports
1 parent 7711bf3 commit 8c70e6d

Some content is hidden

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

52 files changed

+54
-64
lines changed

Diff for: ‎Mathlib.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -353,11 +353,11 @@ import Mathlib.Algebra.Group.PUnit
353353
import Mathlib.Algebra.Group.Pi.Basic
354354
import Mathlib.Algebra.Group.Pi.Lemmas
355355
import Mathlib.Algebra.Group.Pi.Units
356-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
356+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
357357
import Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
358358
import Mathlib.Algebra.Group.Pointwise.Finset.Density
359359
import Mathlib.Algebra.Group.Pointwise.Finset.Interval
360-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
360+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
361361
import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
362362
import Mathlib.Algebra.Group.Pointwise.Set.Card
363363
import Mathlib.Algebra.Group.Pointwise.Set.Finite

Diff for: ‎Mathlib/Algebra/AddTorsor/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Joseph Myers, Yury Kudryashov
66
import Mathlib.Algebra.AddTorsor.Defs
77
import Mathlib.Algebra.Group.Action.Basic
88
import Mathlib.Algebra.Group.End
9-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
9+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
1010

1111
/-!
1212
# Torsors of additive group actions

Diff for: ‎Mathlib/Algebra/Algebra/Operations.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Kenny Lau
55
-/
66
import Mathlib.Algebra.Algebra.Bilinear
77
import Mathlib.Algebra.Algebra.Opposite
8-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
8+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
99
import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
1010
import Mathlib.Algebra.Module.Submodule.Pointwise
1111
import Mathlib.Algebra.Ring.NonZeroDivisors

Diff for: ‎Mathlib/Algebra/BigOperators/Expect.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Algebra.Rat
77
import Mathlib.Algebra.BigOperators.GroupWithZero.Action
88
import Mathlib.Algebra.BigOperators.Pi
99
import Mathlib.Algebra.BigOperators.Ring.Finset
10-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
10+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
1111
import Mathlib.Algebra.Module.Pi
1212
import Mathlib.Data.Finset.Density
1313
import Mathlib.Data.Fintype.BigOperators

Diff for: ‎Mathlib/Algebra/Group/Action/Equidecomp.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Felix Weilacher
55
-/
66
import Mathlib.Algebra.Group.Action.Defs
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88
import Mathlib.Logic.Equiv.PartialEquiv
99

1010
/-!

Diff for: ‎Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Floris van Doorn, Yaël Dillies
55
-/
66
import Mathlib.Algebra.Group.Action.Pi
77
import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
8-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
8+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
99

1010
/-!
1111
# Pointwise actions of finsets

Diff for: ‎Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Johan Commelin, Floris van Doorn, Yaël Dillies
55
-/
66
import Mathlib.Algebra.Group.Action.Basic
77
import Mathlib.Algebra.Group.Action.Opposite
8-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
8+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
99
import Mathlib.Algebra.Group.Units.Equiv
1010
import Mathlib.Data.Set.Lattice.Image
1111
import Mathlib.Data.Set.Pairwise.Basic

Diff for: ‎Mathlib/Algebra/Group/Action/Pointwise/Set/Finite.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import Mathlib.Algebra.Group.Action.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
88
import Mathlib.Data.Set.Finite.Basic
99

1010
/-! # Finiteness lemmas for pointwise operations on sets -/

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Finset/BigOperators.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn, Yaël Dillies
55
-/
66
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88

99
/-!
1010
# Pointwise big operators on finsets

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Finset/Density.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn, Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Group.Action.Pointwise.Finset
88
import Mathlib.Algebra.Group.Action.Defs
99
import Mathlib.Data.Finset.Density

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Wieser
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Order.Group.Pointwise.Interval
88
import Mathlib.Order.Interval.Finset.Defs
99

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

-5
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,6 @@ For sets `s` and `t` and scalar `a`:
2222
* `-s`: Negation, set of all `-x` where `x ∈ s`.
2323
* `s / t`: Division, set of all `x / y` where `x ∈ s` and `y ∈ t`.
2424
* `s - t`: Subtraction, set of all `x - y` where `x ∈ s` and `y ∈ t`.
25-
* `s • t`: Scalar multiplication, set of all `x • y` where `x ∈ s` and `y ∈ t`.
26-
* `s +ᵥ t`: Scalar addition, set of all `x +ᵥ y` where `x ∈ s` and `y ∈ t`.
27-
* `s -ᵥ t`: Scalar subtraction, set of all `x -ᵥ y` where `x ∈ s` and `y ∈ t`.
28-
* `a • s`: Scaling, set of all `a • x` where `x ∈ s`.
29-
* `a +ᵥ s`: Translation, set of all `a +ᵥ x` where `x ∈ s`.
3025
3126
For `α` a semigroup/monoid, `Set α` is a semigroup/monoid.
3227
As an unfortunate side effect, this means that `n • s`, where `n : ℕ`, is ambiguous between

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Wieser
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Data.Fintype.Card
88
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
99

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/Finite.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Data.Finite.Prod
88

99
/-! # Finiteness lemmas for pointwise operations on sets -/

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/Lattice.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Floris van Doorn, Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Data.Set.Lattice.Image
88

99
/-!

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Wieser
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Data.List.OfFn
88
import Mathlib.Algebra.BigOperators.Group.List.Defs
99

Diff for: ‎Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean

+3-8
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,14 @@ Authors: Johan Commelin, Floris van Doorn, Yaël Dillies
66
import Mathlib.Algebra.Group.Pointwise.Set.Basic
77

88
/-!
9-
# Pointwise operations of sets
9+
# Pointwise scalar operations of sets
1010
11-
This file defines pointwise algebraic operations on sets.
11+
This file defines pointwise scalar-flavored algebraic operations on sets.
1212
1313
## Main declarations
1414
1515
For sets `s` and `t` and scalar `a`:
16-
* `s * t`: Multiplication, set of all `x * y` where `x ∈ s` and `y ∈ t`.
17-
* `s + t`: Addition, set of all `x + y` where `x ∈ s` and `y ∈ t`.
18-
* `s⁻¹`: Inversion, set of all `x⁻¹` where `x ∈ s`.
19-
* `-s`: Negation, set of all `-x` where `x ∈ s`.
20-
* `s / t`: Division, set of all `x / y` where `x ∈ s` and `y ∈ t`.
21-
* `s - t`: Subtraction, set of all `x - y` where `x ∈ s` and `y ∈ t`.
16+
2217
* `s • t`: Scalar multiplication, set of all `x • y` where `x ∈ s` and `y ∈ t`.
2318
* `s +ᵥ t`: Scalar addition, set of all `x +ᵥ y` where `x ∈ s` and `y ∈ t`.
2419
* `s -ᵥ t`: Scalar subtraction, set of all `x -ᵥ y` where `x ∈ s` and `y ∈ t`.

Diff for: ‎Mathlib/Algebra/Group/UniqueProds/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Damiano Testa
55
-/
66
import Mathlib.Algebra.FreeMonoid.Basic
77
import Mathlib.Algebra.Group.Equiv.Opposite
8-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
8+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
99
import Mathlib.Algebra.Group.TypeTags.Basic
1010
import Mathlib.Algebra.Group.ULift
1111
import Mathlib.Algebra.Order.Group.Nat

Diff for: ‎Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies, Bhavik Mehta
55
-/
66
import Mathlib.Algebra.GroupWithZero.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88

99
/-!
1010
# Pointwise operations of finsets in a group with zero

Diff for: ‎Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Floris van Doorn
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.GroupWithZero.Basic
88

99
/-!

Diff for: ‎Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.GroupWithZero.Action.Basic
88
import Mathlib.SetTheory.Cardinal.Finite
99

Diff for: ‎Mathlib/Algebra/MonoidAlgebra/Support.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Damiano Testa
55
-/
66
import Mathlib.Algebra.Group.Embedding
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88
import Mathlib.Algebra.MonoidAlgebra.Defs
99
import Mathlib.LinearAlgebra.Finsupp.Supported
1010

Diff for: ‎Mathlib/Algebra/Order/Antidiag/Pi.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Eric Wieser, Bhavik Mehta,
55
Yaël Dillies
66
-/
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88
import Mathlib.Algebra.Order.BigOperators.Group.Finset
99
import Mathlib.Data.Fin.Tuple.NatAntidiagonal
1010
import Mathlib.Data.Finset.Sym

Diff for: ‎Mathlib/Algebra/Order/Field/Pointwise.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Alex J. Best. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alex J. Best, Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.GroupWithZero.Action.Defs
88
import Mathlib.Algebra.Order.Field.Defs
99
import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas

Diff for: ‎Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Order.Group.OrderIso
88
import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
99
import Mathlib.Order.Bounds.OrderIso

Diff for: ‎Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov, Patrick Massot
55
-/
66
import Mathlib.Algebra.Group.Action.Defs
7-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
88
import Mathlib.Algebra.Order.Field.Basic
99
import Mathlib.Algebra.Order.Group.MinMax
1010
import Mathlib.Algebra.Order.Interval.Set.Monoid

Diff for: ‎Mathlib/Algebra/Order/Interval/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Ring.Prod
88
import Mathlib.Algebra.Order.BigOperators.Group.Finset
99
import Mathlib.Algebra.Order.Ring.Canonical

Diff for: ‎Mathlib/Algebra/Order/Module/Pointwise.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Order.Module.Defs
88
import Mathlib.Order.Bounds.OrderIso
99
import Mathlib.Order.GaloisConnection.Basic

Diff for: ‎Mathlib/Algebra/Ring/Action/Pointwise/Finset.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Module.Defs
88

99
/-!

Diff for: ‎Mathlib/Algebra/Ring/Action/Pointwise/Set.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Module.Defs
88

99
/-!

Diff for: ‎Mathlib/Algebra/Ring/Pointwise/Finset.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Ring.Pointwise.Set
88
import Mathlib.Algebra.Ring.InjSurj
99

Diff for: ‎Mathlib/Algebra/Ring/Pointwise/Set.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Floris van Doorn
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Ring.Defs
88

99
/-!

Diff for: ‎Mathlib/Algebra/Star/Conjneg.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import Mathlib.Algebra.BigOperators.Pi
7-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
88
import Mathlib.Algebra.Star.Pi
99

1010
/-!

Diff for: ‎Mathlib/Algebra/Star/Pointwise.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jireh Loreaux
55
-/
66
import Mathlib.Algebra.Field.Defs
7-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
88
import Mathlib.Algebra.Star.Basic
99
import Mathlib.Data.Set.Finite.Basic
1010
import Mathlib.Data.Set.Lattice.Image

Diff for: ‎Mathlib/Combinatorics/Additive/CovBySMul.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88
import Mathlib.Data.Real.Basic
99

1010
/-!

Diff for: ‎Mathlib/Combinatorics/Additive/Dissociation.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
77
import Mathlib.Algebra.Group.Units.Equiv
88
import Mathlib.Data.Fintype.Pi
99
import Mathlib.Data.Finset.Powerset

Diff for: ‎Mathlib/Combinatorics/Additive/Energy.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies, Ella Yu. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies, Ella Yu
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
88
import Mathlib.Data.Finset.Prod
99
import Mathlib.Data.Fintype.Prod

Diff for: ‎Mathlib/Combinatorics/Additive/FreimanHom.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
55
-/
66
import Mathlib.Algebra.BigOperators.Ring.Finset
77
import Mathlib.Algebra.CharP.Basic
8-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
8+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
99
import Mathlib.Algebra.Group.Submonoid.Defs
1010
import Mathlib.Algebra.Order.BigOperators.Group.Multiset
1111
import Mathlib.Algebra.Order.Ring.Nat

Diff for: ‎Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies, George Shakan. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies, George Shakan
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Algebra.Order.Field.Rat
88
import Mathlib.Combinatorics.Enumerative.DoubleCounting
99
import Mathlib.Tactic.FieldSimp

Diff for: ‎Mathlib/Combinatorics/SimpleGraph/Circulant.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Iván Renison, Bhavik Mehta
55
-/
66
import Mathlib.Algebra.Group.Fin.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Set.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
88
import Mathlib.Combinatorics.SimpleGraph.Hasse
99

1010
/-!

Diff for: ‎Mathlib/Data/DFinsupp/Interval.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
6+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
77
import Mathlib.Data.Fintype.BigOperators
88
import Mathlib.Data.DFinsupp.BigOperators
99
import Mathlib.Data.DFinsupp.Order

Diff for: ‎Mathlib/Data/Finset/Finsupp.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import Mathlib.Algebra.BigOperators.Finsupp.Basic
7-
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
7+
import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
88
import Mathlib.Data.Finsupp.Indicator
99
import Mathlib.Data.Fintype.BigOperators
1010

0 commit comments

Comments
 (0)