Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - Acl/reorg tensor product #11282

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - Acl/reorg tensor product #11282

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
3844ac4
Mv DirectLimitAndTensorProduct to another folder and rename
Mar 10, 2024
256e55e
Mv TensorProduct.lean to TensorProduct/Basic.lean
Mar 10, 2024
06e4d01
mv TensorProductBasis.lean to TensorProduct/Basis.lean
Mar 10, 2024
9051c25
mv RingTheory/TensorProduct.lean to RingTheory/TensorProduct/Basic.lean
Mar 10, 2024
400b21a
update Mathlib.lean
Mar 10, 2024
74d63a1
update import line in files importing Mathlib/Algebra/TensorProduct
Mar 10, 2024
c632485
update import line in files importing Mathlib/RingTheory/TensorProduct
Mar 10, 2024
417a468
Update import line about LinearAlgebra/TensorProduct/Basis
Mar 10, 2024
7c1dd7c
update Mathlib.lean
Mar 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
6 changes: 3 additions & 3 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -333,7 +333,6 @@ import Mathlib.Algebra.Module.BigOperators
import Mathlib.Algebra.Module.Bimodule
import Mathlib.Algebra.Module.CharacterModule
import Mathlib.Algebra.Module.DedekindDomain
import Mathlib.Algebra.Module.DirectLimitAndTensorProduct
import Mathlib.Algebra.Module.Equiv
import Mathlib.Algebra.Module.GradedModule
import Mathlib.Algebra.Module.Hom
Expand Down Expand Up @@ -2652,7 +2651,8 @@ import Mathlib.LinearAlgebra.TensorAlgebra.Basis
import Mathlib.LinearAlgebra.TensorAlgebra.Grading
import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
import Mathlib.LinearAlgebra.TensorPower
import Mathlib.LinearAlgebra.TensorProduct
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
AntoineChambert-Loir marked this conversation as resolved.
Show resolved Hide resolved
import Mathlib.LinearAlgebra.TensorProduct.Graded.External
import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
import Mathlib.LinearAlgebra.TensorProduct.Matrix
Expand Down Expand Up @@ -3404,7 +3404,7 @@ import Mathlib.RingTheory.Subring.Units
import Mathlib.RingTheory.Subsemiring.Basic
import Mathlib.RingTheory.Subsemiring.Order
import Mathlib.RingTheory.Subsemiring.Pointwise
import Mathlib.RingTheory.TensorProduct
import Mathlib.RingTheory.TensorProduct.Basic
import Mathlib.RingTheory.Trace
import Mathlib.RingTheory.UniqueFactorizationDomain
import Mathlib.RingTheory.Valuation.Basic
Expand Down
0 Mathlib/LinearAlgebra/TensorProduct.lean → ...ib/LinearAlgebra/TensorProduct/Basic.lean
View file
Open in desktop
File renamed without changes.
0 ...lib/LinearAlgebra/TensorProductBasis.lean → ...ib/LinearAlgebra/TensorProduct/Basis.lean
View file
Open in desktop
File renamed without changes.
0 ...a/Module/DirectLimitAndTensorProduct.lean → ...earAlgebra/TensorProduct/DirectLimit.lean
View file
Open in desktop
File renamed without changes.
0 Mathlib/RingTheory/TensorProduct.lean → Mathlib/RingTheory/TensorProduct/Basic.lean
View file
Open in desktop
File renamed without changes.