From 0c13e18343c06775d5f2121a433f70392b7e2caa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 3 Oct 2024 19:18:22 +0000 Subject: [PATCH] chore: Rename `FiniteDimensional.finrank` to `Module.finrank` (#17192) The namespacing in the linear algebra/affine spaces part of the library is a bit suboptimal. Here are a few arguments for why `FiniteDimensional.finrank` should be renamed to `Module.finrank`: 1. Other objects in maths can be finite-dimensional and have a rank. 2. `finrank` is directly analogous to `Module.rank`, they have lemmas in common (eg `finrank_eq_rank`, which is currently in neither of the declarations' namespaces) and have common series of lemmas that relate to other declarations in the `Module` namespace, eg `Module.Finite`. 3. We are in the process of replacing `FiniteDimensional` by `Module.Finite`, so the `FiniteDimensional` namespace will soon be obsolete. 4. It is a shorter and clearer name. Also make `Module.Finite` protected to avoid clashes with `Finite` --- Archive/Imo/Imo2019Q2.lean | 2 +- Archive/Sensitivity.lean | 2 +- .../Algebra/Subalgebra/IsSimpleOrder.lean | 2 +- Mathlib/Algebra/Algebra/Subalgebra/Rank.lean | 2 +- Mathlib/Algebra/Category/ModuleCat/Free.lean | 10 +- .../Algebra/Category/ModuleCat/Simple.lean | 2 +- Mathlib/Algebra/Lie/CartanExists.lean | 6 +- Mathlib/Algebra/Lie/InvariantForm.lean | 6 +- Mathlib/Algebra/Lie/Rank.lean | 12 +-- Mathlib/Algebra/Lie/TraceForm.lean | 4 +- Mathlib/Algebra/Lie/Weights/Basic.lean | 4 +- Mathlib/Algebra/Lie/Weights/Chain.lean | 2 +- Mathlib/Algebra/Lie/Weights/Killing.lean | 2 +- Mathlib/Algebra/Lie/Weights/Linear.lean | 2 +- .../Algebra/Module/LinearMap/Polynomial.lean | 8 +- Mathlib/Algebra/Module/Submodule/Map.lean | 2 +- Mathlib/Algebra/Module/ZLattice/Basic.lean | 4 +- Mathlib/Algebra/Module/ZLattice/Covolume.lean | 2 +- Mathlib/Algebra/Polynomial/Module/AEval.lean | 7 +- Mathlib/Algebra/Quaternion.lean | 6 +- .../EllipticCurve/Group.lean | 2 +- .../Calculus/BumpFunction/Convolution.lean | 2 +- .../BumpFunction/FiniteDimension.lean | 2 +- .../Calculus/BumpFunction/Normed.lean | 2 +- .../Calculus/ContDiff/FiniteDimension.lean | 2 +- .../LineDeriv/IntegrationByParts.lean | 2 +- Mathlib/Analysis/Calculus/Rademacher.lean | 2 +- Mathlib/Analysis/Convex/Measure.lean | 4 +- Mathlib/Analysis/Convex/Normed.lean | 2 +- Mathlib/Analysis/Convex/Radon.lean | 2 +- .../Analysis/Distribution/SchwartzSpace.lean | 4 +- Mathlib/Analysis/Fourier/Inversion.lean | 2 +- .../Fourier/RiemannLebesgueLemma.lean | 2 +- .../FunctionalSpaces/SobolevInequality.lean | 2 +- Mathlib/Analysis/InnerProductSpace/Basic.lean | 2 +- .../InnerProductSpace/EuclideanDist.lean | 2 +- .../InnerProductSpace/GramSchmidtOrtho.lean | 2 +- .../InnerProductSpace/Orientation.lean | 2 +- Mathlib/Analysis/InnerProductSpace/PiL2.lean | 12 +-- .../InnerProductSpace/Projection.lean | 8 +- .../Analysis/InnerProductSpace/Spectrum.lean | 2 +- .../Analysis/InnerProductSpace/TwoDim.lean | 4 +- .../Normed/Module/FiniteDimension.lean | 8 +- .../NormedSpace/HahnBanach/Extension.lean | 4 +- .../Gaussian/FourierTransform.lean | 10 +- .../SpecialFunctions/JapaneseBracket.lean | 2 +- Mathlib/CategoryTheory/Preadditive/Schur.lean | 2 +- .../Combinatorics/SimpleGraph/LapMatrix.lean | 4 +- Mathlib/Data/Complex/FiniteDimensional.lean | 9 +- Mathlib/Data/Matrix/Rank.lean | 6 +- Mathlib/FieldTheory/Adjoin.lean | 17 ++-- Mathlib/FieldTheory/Cardinality.lean | 4 +- Mathlib/FieldTheory/Finite/Basic.lean | 4 +- Mathlib/FieldTheory/Finite/GaloisField.lean | 4 +- Mathlib/FieldTheory/Finite/Polynomial.lean | 6 +- Mathlib/FieldTheory/Fixed.lean | 2 +- Mathlib/FieldTheory/Galois/Basic.lean | 2 +- .../IntermediateField/Algebraic.lean | 9 +- Mathlib/FieldTheory/IsPerfectClosure.lean | 2 +- Mathlib/FieldTheory/KummerExtension.lean | 10 +- Mathlib/FieldTheory/Minpoly/Field.lean | 6 +- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean | 2 +- .../FieldTheory/PolynomialGaloisGroup.lean | 6 +- Mathlib/FieldTheory/PrimitiveElement.lean | 6 +- Mathlib/FieldTheory/PurelyInseparable.lean | 4 +- Mathlib/FieldTheory/SeparableClosure.lean | 2 +- Mathlib/FieldTheory/SeparableDegree.lean | 14 +-- Mathlib/FieldTheory/Tower.lean | 2 +- .../Euclidean/Angle/Oriented/Affine.lean | 2 +- .../Euclidean/Angle/Oriented/Basic.lean | 2 +- .../Euclidean/Angle/Oriented/RightAngle.lean | 4 +- .../Euclidean/Angle/Oriented/Rotation.lean | 8 +- Mathlib/Geometry/Euclidean/Angle/Sphere.lean | 2 +- Mathlib/Geometry/Euclidean/Basic.lean | 4 +- Mathlib/Geometry/Euclidean/Circumcenter.lean | 2 +- Mathlib/Geometry/Euclidean/MongePoint.lean | 13 +-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean | 2 +- Mathlib/Geometry/Euclidean/Triangle.lean | 2 +- Mathlib/Geometry/Manifold/BumpFunction.lean | 2 +- .../Geometry/Manifold/Instances/Sphere.lean | 2 +- .../Geometry/Manifold/PartitionOfUnity.lean | 2 +- .../Geometry/Manifold/WhitneyEmbedding.lean | 2 +- .../AffineSpace/FiniteDimensional.lean | 16 +-- .../BilinearForm/Orthogonal.lean | 2 +- Mathlib/LinearAlgebra/Charpoly/Basic.lean | 2 +- Mathlib/LinearAlgebra/Coevaluation.lean | 2 +- Mathlib/LinearAlgebra/Contraction.lean | 2 +- Mathlib/LinearAlgebra/Determinant.lean | 16 +-- .../Dimension/Constructions.lean | 22 ++--- .../LinearAlgebra/Dimension/DivisionRing.lean | 4 +- Mathlib/LinearAlgebra/Dimension/Finite.lean | 24 ++--- Mathlib/LinearAlgebra/Dimension/Finrank.lean | 10 +- Mathlib/LinearAlgebra/Dimension/Free.lean | 37 +++---- .../Dimension/FreeAndStrongRankCondition.lean | 6 +- .../LinearAlgebra/Dimension/Localization.lean | 4 +- .../LinearAlgebra/Dimension/RankNullity.lean | 2 +- .../Dimension/StrongRankCondition.lean | 34 +++---- Mathlib/LinearAlgebra/Dual.lean | 25 ++--- Mathlib/LinearAlgebra/Eigenspace/Basic.lean | 2 +- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean | 2 +- .../Eigenspace/Triangularizable.lean | 2 +- Mathlib/LinearAlgebra/Eigenspace/Zero.lean | 2 +- Mathlib/LinearAlgebra/FiniteDimensional.lean | 6 +- .../LinearAlgebra/FiniteDimensional/Defs.lean | 99 +++++++++---------- .../FreeModule/Finite/Matrix.lean | 16 +-- .../FreeModule/IdealQuotient.lean | 6 +- Mathlib/LinearAlgebra/FreeModule/Norm.lean | 2 +- .../Matrix/GeneralLinearGroup/Card.lean | 6 +- Mathlib/LinearAlgebra/Orientation.lean | 2 +- .../LinearAlgebra/Projectivization/Basic.lean | 2 +- .../LinearAlgebra/QuadraticForm/Basic.lean | 4 +- .../LinearAlgebra/QuadraticForm/Complex.lean | 2 +- .../QuadraticForm/IsometryEquiv.lean | 6 +- Mathlib/LinearAlgebra/QuadraticForm/Real.lean | 8 +- Mathlib/LinearAlgebra/Semisimple.lean | 8 +- .../TensorProduct/Subalgebra.lean | 6 +- Mathlib/LinearAlgebra/Trace.lean | 2 +- .../Constructions/HaarToSphere.lean | 8 +- .../Covering/BesicovitchVectorSpace.lean | 2 +- Mathlib/MeasureTheory/Function/Jacobian.lean | 4 +- .../Group/GeometryOfNumbers.lean | 2 +- .../MeasureTheory/Integral/PeakFunction.lean | 2 +- .../Measure/Haar/InnerProductSpace.lean | 2 +- .../Measure/Haar/NormedSpace.lean | 6 +- .../MeasureTheory/Measure/Haar/OfBasis.lean | 2 +- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 2 +- .../Measure/Lebesgue/EqHaar.lean | 2 +- .../Measure/Lebesgue/VolumeOfBalls.lean | 6 +- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 2 +- .../NumberTheory/Cyclotomic/Embeddings.lean | 2 +- .../Cyclotomic/PrimitiveRoots.lean | 6 +- Mathlib/NumberTheory/FunctionField.lean | 4 +- Mathlib/NumberTheory/NumberField/Basic.lean | 2 +- .../NumberField/CanonicalEmbedding/Basic.lean | 6 +- .../CanonicalEmbedding/ConvexBody.lean | 4 +- .../CanonicalEmbedding/FundamentalCone.lean | 2 +- .../NumberTheory/NumberField/ClassNumber.lean | 2 +- .../NumberField/Discriminant.lean | 2 +- .../NumberTheory/NumberField/Embeddings.lean | 14 +-- .../NumberField/EquivReindex.lean | 2 +- .../NumberField/FractionalIdeal.lean | 2 +- Mathlib/NumberTheory/NumberField/House.lean | 4 +- Mathlib/NumberTheory/NumberField/Norm.lean | 2 +- .../NumberField/Units/DirichletTheorem.lean | 6 +- Mathlib/NumberTheory/RamificationInertia.lean | 4 +- Mathlib/RepresentationTheory/Character.lean | 4 +- Mathlib/RepresentationTheory/FDRep.lean | 2 +- .../DedekindDomain/IntegralClosure.lean | 4 +- .../DiscreteValuationRing/TFAE.lean | 2 +- Mathlib/RingTheory/Discriminant.lean | 4 +- Mathlib/RingTheory/FiniteType.lean | 4 +- Mathlib/RingTheory/Finiteness.lean | 41 ++++---- .../RingTheory/Flat/EquationalCriterion.lean | 14 +-- Mathlib/RingTheory/Ideal/Cotangent.lean | 2 +- Mathlib/RingTheory/LittleWedderburn.lean | 2 +- Mathlib/RingTheory/LocalRing/Module.lean | 8 +- Mathlib/RingTheory/Noetherian.lean | 6 +- Mathlib/RingTheory/Norm/Basic.lean | 4 +- Mathlib/RingTheory/Norm/Defs.lean | 2 +- .../Polynomial/Eisenstein/IsIntegral.lean | 2 +- Mathlib/RingTheory/PowerBasis.lean | 6 +- Mathlib/RingTheory/SimpleModule.lean | 2 +- Mathlib/RingTheory/Trace/Basic.lean | 4 +- Mathlib/RingTheory/Trace/Defs.lean | 2 +- Mathlib/RingTheory/Valuation/Minpoly.lean | 2 +- Mathlib/RingTheory/WittVector/Isocrystal.lean | 4 +- .../Algebra/Module/FiniteDimension.lean | 6 +- .../MetricSpace/HausdorffDimension.lean | 6 +- 168 files changed, 477 insertions(+), 500 deletions(-) diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean index db1650a221391..86353bd5b6d91 100644 --- a/Archive/Imo/Imo2019Q2.lean +++ b/Archive/Imo/Imo2019Q2.lean @@ -57,7 +57,7 @@ rather than more literally with `affineSegment`. -/ -open Affine Affine.Simplex EuclideanGeometry FiniteDimensional +open Affine Affine.Simplex EuclideanGeometry Module open scoped Affine EuclideanGeometry Real diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index d28ffea139084..5cae8d062537c 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -41,7 +41,7 @@ noncomputable section local notation "√" => Real.sqrt -open Function Bool LinearMap Fintype FiniteDimensional Module.DualBases +open Function Bool LinearMap Fintype Module Module.DualBases /-! ### The hypercube diff --git a/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean b/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean index 468781008d3b8..2c9016caf3b6c 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean @@ -12,7 +12,7 @@ If `A` is a domain, and a finite-dimensional algebra over a field `F`, with prim then there are no non-trivial `F`-subalgebras. -/ -open FiniteDimensional Submodule +open Module Submodule theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A] [Algebra F A] (hp : (finrank F A).Prime) : IsSimpleOrder (Subalgebra F A) := diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean index 1dac252bbf591..e4b3c91e4d894 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean @@ -18,7 +18,7 @@ satisfies strong rank condition, we put them into a separate file. -/ -open FiniteDimensional +open Module namespace Subalgebra diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean index 0cf3303dd9713..9f822325b9425 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Free.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Free.lean @@ -26,7 +26,7 @@ linear algebra, module, free -/ -open CategoryTheory +open CategoryTheory Module namespace ModuleCat @@ -177,11 +177,11 @@ theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃] theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃] [Module.Finite R S.X₁] [Module.Finite R S.X₃] - (hN : FiniteDimensional.finrank R S.X₁ = n) - (hP : FiniteDimensional.finrank R S.X₃ = p) + (hN : Module.finrank R S.X₁ = n) + (hP : Module.finrank R S.X₃ = p) [StrongRankCondition R] : - FiniteDimensional.finrank R S.X₂ = n + p := by - apply FiniteDimensional.finrank_eq_of_rank_eq + finrank R S.X₂ = n + p := by + apply finrank_eq_of_rank_eq rw [free_shortExact_rank_add hS', ← hN, ← hP] simp only [Nat.cast_add, finrank_eq_rank] diff --git a/Mathlib/Algebra/Category/ModuleCat/Simple.lean b/Mathlib/Algebra/Category/ModuleCat/Simple.lean index dcccbac0230b4..a36bd8151ab84 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Simple.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Simple.lean @@ -34,7 +34,7 @@ instance simple_of_isSimpleModule [IsSimpleModule R M] : Simple (of R M) := instance isSimpleModule_of_simple (M : ModuleCat R) [Simple M] : IsSimpleModule R M := simple_iff_isSimpleModule.mp (Simple.of_iso (ofSelfIso M)) -open FiniteDimensional +open Module attribute [local instance] moduleOfAlgebraModule isScalarTower_of_algebra_moduleCat diff --git a/Mathlib/Algebra/Lie/CartanExists.lean b/Mathlib/Algebra/Lie/CartanExists.lean index ae5ba4fc34d14..5ee149734e3b5 100644 --- a/Mathlib/Algebra/Lie/CartanExists.lean +++ b/Mathlib/Algebra/Lie/CartanExists.lean @@ -39,7 +39,7 @@ variable [Module.Finite K L] variable [Module.Finite R L] [Module.Free R L] variable [Module.Finite R M] [Module.Free R M] -open FiniteDimensional LieSubalgebra Module.Free Polynomial +open Module LieSubalgebra Module.Free Polynomial variable (K) @@ -117,7 +117,7 @@ section Field variable {K L : Type*} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] -open FiniteDimensional LieSubalgebra LieSubmodule Polynomial Cardinal LieModule engel_isBot_of_isMin +open Module LieSubalgebra LieSubmodule Polynomial Cardinal LieModule engel_isBot_of_isMin #adaptation_note /-- otherwise there is a spurious warning on `contrapose!` below. -/ set_option linter.unusedVariables false in @@ -360,7 +360,7 @@ lemma exists_isCartanSubalgebra_engel_of_finrank_le_card (h : finrank K L ≤ #K suffices finrank K (engel K x) ≤ finrank K (engel K y) by suffices engel K y = engel K x from this.ge apply LieSubalgebra.to_submodule_injective - exact eq_of_le_of_finrank_le hyx this + exact Submodule.eq_of_le_of_finrank_le hyx this rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx] apply rank_le_finrank_engel diff --git a/Mathlib/Algebra/Lie/InvariantForm.lean b/Mathlib/Algebra/Lie/InvariantForm.lean index dea6e6da8c49d..e95fdc8b0f1bf 100644 --- a/Mathlib/Algebra/Lie/InvariantForm.lean +++ b/Mathlib/Algebra/Lie/InvariantForm.lean @@ -124,14 +124,14 @@ variable (hΦ_inv : Φ.lieInvariant L) (hΦ_refl : Φ.IsRefl) variable (hL : ∀ I : LieIdeal K L, IsAtom I → ¬IsLieAbelian I) include hΦ_nondeg hΦ_refl hL -open FiniteDimensional Submodule in +open Module Submodule in lemma orthogonal_isCompl_coe_submodule (I : LieIdeal K L) (hI : IsAtom I) : IsCompl I.toSubmodule (orthogonal Φ hΦ_inv I).toSubmodule := by rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl, ← orthogonal_toSubmodule _ hΦ_inv, ← LieSubmodule.disjoint_iff_coe_toSubmodule] exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI -open FiniteDimensional Submodule in +open Module Submodule in lemma orthogonal_isCompl (I : LieIdeal K L) (hI : IsAtom I) : IsCompl I (orthogonal Φ hΦ_inv I) := by rw [LieSubmodule.isCompl_iff_coe_toSubmodule] @@ -151,7 +151,7 @@ lemma restrict_orthogonal_nondegenerate (I : LieIdeal K L) (hI : IsAtom I) : LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl] exact (orthogonal_isCompl_coe_submodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm -open FiniteDimensional Submodule in +open Module Submodule in lemma atomistic : ∀ I : LieIdeal K L, sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I := by intro I apply le_antisymm diff --git a/Mathlib/Algebra/Lie/Rank.lean b/Mathlib/Algebra/Lie/Rank.lean index 3fabb5568a84c..c9c5877344913 100644 --- a/Mathlib/Algebra/Lie/Rank.lean +++ b/Mathlib/Algebra/Lie/Rank.lean @@ -65,13 +65,13 @@ lemma rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] : rank R L M = (polyCharpoly φ b).natTrailingDegree := by apply nilRank_eq_polyCharpoly_natTrailingDegree -open FiniteDimensional +open Module include bₘ in lemma rank_le_card [Nontrivial R] : rank R L M ≤ Fintype.card ιₘ := nilRank_le_card _ bₘ -open FiniteDimensional +open Module lemma rank_le_finrank [Nontrivial R] : rank R L M ≤ finrank R M := nilRank_le_finrank _ @@ -103,7 +103,7 @@ section IsDomain variable (L) variable [IsDomain R] -open Cardinal FiniteDimensional MvPolynomial in +open Cardinal Module MvPolynomial in lemma exists_isRegular_of_finrank_le_card (h : finrank R M ≤ #R) : ∃ x : L, IsRegular R M x := LinearMap.exists_isNilRegular_of_finrank_le_card _ h @@ -138,7 +138,7 @@ lemma rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] : rank R L = (polyCharpoly (ad R L).toLinearMap b).natTrailingDegree := by apply nilRank_eq_polyCharpoly_natTrailingDegree -open FiniteDimensional +open Module include b in lemma rank_le_card [Nontrivial R] : rank R L ≤ Fintype.card ι := @@ -175,7 +175,7 @@ section IsDomain variable (L) variable [IsDomain R] -open Cardinal FiniteDimensional MvPolynomial in +open Cardinal Module MvPolynomial in lemma exists_isRegular_of_finrank_le_card (h : finrank R L ≤ #R) : ∃ x : L, IsRegular R x := LinearMap.exists_isNilRegular_of_finrank_le_card _ h @@ -191,7 +191,7 @@ namespace LieAlgebra variable (K : Type*) {L : Type*} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] -open FiniteDimensional LieSubalgebra +open Module LieSubalgebra lemma finrank_engel (x : L) : finrank K (engel K x) = (ad K L x).charpoly.natTrailingDegree := diff --git a/Mathlib/Algebra/Lie/TraceForm.lean b/Mathlib/Algebra/Lie/TraceForm.lean index b7b439cf4ddfd..3e6c88e8e9ed1 100644 --- a/Mathlib/Algebra/Lie/TraceForm.lean +++ b/Mathlib/Algebra/Lie/TraceForm.lean @@ -38,7 +38,7 @@ variable (R K L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L] local notation "φ" => LieModule.toEnd R L M open LinearMap (trace) -open Set FiniteDimensional +open Set Module namespace LieModule @@ -392,7 +392,7 @@ lemma killingForm_eq : end LieIdeal -open LieModule FiniteDimensional +open LieModule Module open Submodule (span subset_span) namespace LieModule diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean index 810246b2c95a8..bebee81c0475c 100644 --- a/Mathlib/Algebra/Lie/Weights/Basic.lean +++ b/Mathlib/Algebra/Lie/Weights/Basic.lean @@ -745,7 +745,7 @@ lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) : simp_rw [Module.End.maxGenEigenspace_def] exact IsTriangularizable.iSup_eq_top x -open LinearMap FiniteDimensional in +open LinearMap Module in @[simp] lemma trace_toEnd_genWeightSpace [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] (χ : L → R) (x : L) : @@ -759,7 +759,7 @@ lemma trace_toEnd_genWeightSpace [IsDomain R] [IsPrincipalIdealRing R] section field -open FiniteDimensional +open Module variable (K) variable [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.IsNilpotent K L] diff --git a/Mathlib/Algebra/Lie/Weights/Chain.lean b/Mathlib/Algebra/Lie/Weights/Chain.lean index bf2671f9c4c4b..428b6ff73884c 100644 --- a/Mathlib/Algebra/Lie/Weights/Chain.lean +++ b/Mathlib/Algebra/Lie/Weights/Chain.lean @@ -41,7 +41,7 @@ We provide basic definitions and results to support `α`-chain techniques in thi -/ -open FiniteDimensional Function Set +open Module Function Set variable {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] diff --git a/Mathlib/Algebra/Lie/Weights/Killing.lean b/Mathlib/Algebra/Lie/Weights/Killing.lean index a941003c52c63..7b0522b1c70b9 100644 --- a/Mathlib/Algebra/Lie/Weights/Killing.lean +++ b/Mathlib/Algebra/Lie/Weights/Killing.lean @@ -85,7 +85,7 @@ end IsKilling section Field -open FiniteDimensional LieModule Set +open Module LieModule Set open Submodule (span subset_span) variable [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean index a4da88d28a011..9798876d617f9 100644 --- a/Mathlib/Algebra/Lie/Weights/Linear.lean +++ b/Mathlib/Algebra/Lie/Weights/Linear.lean @@ -114,7 +114,7 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R section FiniteDimensional -open FiniteDimensional +open Module variable [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] [LieAlgebra.IsNilpotent R L] diff --git a/Mathlib/Algebra/Module/LinearMap/Polynomial.lean b/Mathlib/Algebra/Module/LinearMap/Polynomial.lean index 6f0b08d7782c3..823b874234f59 100644 --- a/Mathlib/Algebra/Module/LinearMap/Polynomial.lean +++ b/Mathlib/Algebra/Module/LinearMap/Polynomial.lean @@ -351,7 +351,7 @@ lemma polyCharpolyAux_basisIndep {ιM' : Type*} [Fintype ιM'] [DecidableEq ιM' end aux -open FiniteDimensional Matrix +open Module Matrix variable [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) @@ -479,11 +479,11 @@ lemma polyCharpoly_coeff_nilRank_ne_zero : rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b] apply polyCharpoly_coeff_nilRankAux_ne_zero -open FiniteDimensional Module.Free +open Module Module.Free lemma nilRank_le_card {ι : Type*} [Fintype ι] (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι := by apply Polynomial.natTrailingDegree_le_of_ne_zero - rw [← FiniteDimensional.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L), + rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L), Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff] apply one_ne_zero @@ -538,7 +538,7 @@ section IsDomain variable [IsDomain R] -open Cardinal FiniteDimensional MvPolynomial Module.Free in +open Cardinal Module MvPolynomial Module.Free in lemma exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) : ∃ x : L, IsNilRegular φ x := by let b := chooseBasis R L diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean index 1d1245ea336c6..0e08a969e1c07 100644 --- a/Mathlib/Algebra/Module/Submodule/Map.lean +++ b/Mathlib/Algebra/Module/Submodule/Map.lean @@ -104,7 +104,7 @@ theorem map_mono {f : F} {p p' : Submodule R M} : p ≤ p' → map f p ≤ map f image_subset _ @[simp] -theorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥ := +protected theorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥ := have : ∃ x : M, x ∈ p := ⟨0, p.zero_mem⟩ ext <| by simp [this, eq_comm] diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean index 0ae1e6609864d..a436852b2ab88 100644 --- a/Mathlib/Algebra/Module/ZLattice/Basic.lean +++ b/Mathlib/Algebra/Module/ZLattice/Basic.lean @@ -384,7 +384,7 @@ end ZSpan section ZLattice -open Submodule FiniteDimensional ZSpan +open Submodule Module ZSpan -- TODO: generalize this class to other rings than `ℤ` /-- `L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if @@ -562,7 +562,7 @@ variable {ι : Type*} [hs : IsZLattice K L] (b : Basis ι ℤ L) /-- Any `ℤ`-basis of `L` is also a `K`-basis of `E`. -/ def Basis.ofZLatticeBasis : Basis ι K E := by - have : Finite ℤ L := ZLattice.module_finite K L + have : Module.Finite ℤ L := ZLattice.module_finite K L have : Free ℤ L := ZLattice.module_free K L let e := Basis.indexEquiv (Free.chooseBasis ℤ L) b have : Fintype ι := Fintype.ofEquiv _ e diff --git a/Mathlib/Algebra/Module/ZLattice/Covolume.lean b/Mathlib/Algebra/Module/ZLattice/Covolume.lean index bec47d37fcc0b..04e559d80a384 100644 --- a/Mathlib/Algebra/Module/ZLattice/Covolume.lean +++ b/Mathlib/Algebra/Module/ZLattice/Covolume.lean @@ -29,7 +29,7 @@ noncomputable section namespace ZLattice -open Submodule MeasureTheory FiniteDimensional MeasureTheory Module +open Submodule MeasureTheory Module MeasureTheory Module section General diff --git a/Mathlib/Algebra/Polynomial/Module/AEval.lean b/Mathlib/Algebra/Polynomial/Module/AEval.lean index daa261800b354..17b934cb8564e 100644 --- a/Mathlib/Algebra/Polynomial/Module/AEval.lean +++ b/Mathlib/Algebra/Polynomial/Module/AEval.lean @@ -46,7 +46,8 @@ instance instAddCommMonoid : AddCommMonoid <| AEval R M a := inferInstanceAs (Ad instance instModuleOrig : Module R <| AEval R M a := inferInstanceAs (Module R M) -instance instFiniteOrig [Finite R M] : Finite R <| AEval R M a := inferInstanceAs (Finite R M) +instance instFiniteOrig [Module.Finite R M] : Module.Finite R <| AEval R M a := + ‹Module.Finite R M› instance instModulePolynomial : Module R[X] <| AEval R M a := compHom M (aeval a).toRingHom @@ -79,7 +80,7 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w apply (of R M a).symm.injective rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul] -instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a := +instance instFinitePolynomial [Module.Finite R M] : Module.Finite R[X] <| AEval R M a := Finite.of_restrictScalars_finite R _ _ /-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/ @@ -193,6 +194,6 @@ lemma AEval'.X_smul_of (m : M) : (X : R[X]) • AEval'.of φ m = AEval'.of φ ( lemma AEval'.of_symm_X_smul (m : AEval' φ) : (AEval'.of φ).symm ((X : R[X]) • m) = φ ((AEval'.of φ).symm m) := AEval.of_symm_X_smul _ _ -instance [Finite R M] : Finite R[X] <| AEval' φ := inferInstance +instance [Module.Finite R M] : Module.Finite R[X] <| AEval' φ := inferInstance end Module diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index a063ebfdef089..f78db6c9f424a 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -569,8 +569,8 @@ theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] = rw [rank_eq_card_basis (basisOneIJK c₁ c₂), Fintype.card_fin] norm_num -theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4 := by - rw [FiniteDimensional.finrank, rank_eq_four, Cardinal.toNat_ofNat] +theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R,c₁,c₂] = 4 := by + rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat] /-- There is a natural equivalence when swapping the coefficients of a quaternion algebra. -/ @[simps] @@ -1024,7 +1024,7 @@ instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,-1] theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R] = 4 := QuaternionAlgebra.rank_eq_four _ _ -theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R] = 4 := +theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R] = 4 := QuaternionAlgebra.finrank_eq_four _ _ @[simp] theorem star_re : (star a).re = a.re := rfl diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean index cbb5edf60ed85..28d32c6a3fea5 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean @@ -545,7 +545,7 @@ lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 := by rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0, ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq, (CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq, - FiniteDimensional.finrank_self] + Module.finrank_self] · exact congr_arg toClass lemma toClass_injective : Function.Injective <| @toClass _ _ W := by diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean b/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean index 6640b13a2e378..4b70bd94ec863 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean @@ -115,7 +115,7 @@ theorem ae_convolution_tendsto_right_of_locallyIntegrable tendsto_nhdsWithin_iff.2 ⟨hφ, Eventually.of_forall (fun i ↦ (φ i).rOut_pos)⟩ have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ' simp only [Function.comp] at this - apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (FiniteDimensional.finrank ℝ G)) this + apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this · filter_upwards with i using hg.integrableOn_isCompact (isCompact_closedBall _ _) · apply tendsto_const_nhds.congr (fun i ↦ ?_) diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean index a246268057e33..d0f390973978c 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean @@ -25,7 +25,7 @@ the indicator function of `closedBall 0 1` with a function as above with `s = ba noncomputable section -open Set Metric TopologicalSpace Function Asymptotics MeasureTheory FiniteDimensional +open Set Metric TopologicalSpace Function Asymptotics MeasureTheory Module ContinuousLinearMap Filter MeasureTheory.Measure Bornology open scoped Pointwise Topology NNReal Convolution diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean b/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean index 1846ced215ae9..a61f635da6766 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean @@ -16,7 +16,7 @@ In this file we define `ContDiffBump.normed f μ` to be the bump function `f` no noncomputable section -open Function Filter Set Metric MeasureTheory FiniteDimensional Measure +open Function Filter Set Metric MeasureTheory Module Measure open scoped Topology namespace ContDiffBump diff --git a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean index 7b0d3e391e4fd..5b3ed3d9a9e4f 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean @@ -24,7 +24,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddC section FiniteDimensional -open Function FiniteDimensional +open Function Module variable [CompleteSpace 𝕜] diff --git a/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean b/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean index 6d2876fdc8402..81863eb235bbc 100644 --- a/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean +++ b/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean @@ -44,7 +44,7 @@ TODO: prove similar theorems assuming that the functions tend to zero at infinit integrable derivatives. -/ -open MeasureTheory Measure FiniteDimensional +open MeasureTheory Measure Module variable {E F G W : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] diff --git a/Mathlib/Analysis/Calculus/Rademacher.lean b/Mathlib/Analysis/Calculus/Rademacher.lean index b1924f51dde25..260a55686a38c 100644 --- a/Mathlib/Analysis/Calculus/Rademacher.lean +++ b/Mathlib/Analysis/Calculus/Rademacher.lean @@ -42,7 +42,7 @@ See `LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure`. * [Pertti Mattila, Geometry of sets and measures in Euclidean spaces, Theorem 7.3][Federer1996] -/ -open Filter MeasureTheory Measure FiniteDimensional Metric Set Asymptotics +open Filter MeasureTheory Measure Module Metric Set Asymptotics open scoped NNReal ENNReal Topology diff --git a/Mathlib/Analysis/Convex/Measure.lean b/Mathlib/Analysis/Convex/Measure.lean index d8b9b78be2d4b..cf276ed3f8958 100644 --- a/Mathlib/Analysis/Convex/Measure.lean +++ b/Mathlib/Analysis/Convex/Measure.lean @@ -18,7 +18,7 @@ convex set in `E`. Then the frontier of `s` has measure zero (see `Convex.addHaa open MeasureTheory MeasureTheory.Measure Set Metric Filter Bornology -open FiniteDimensional (finrank) +open Module (finrank) open scoped Topology NNReal ENNReal @@ -64,7 +64,7 @@ theorem addHaar_frontier (hs : Convex ℝ s) : μ (frontier s) = 0 := by /- Due to `Convex.closure_subset_image_homothety_interior_of_one_lt`, for any `r > 1` we have `closure s ⊆ homothety x r '' interior s`, hence `μ (closure s) ≤ r ^ d * μ (interior s)`, where `d = finrank ℝ E`. -/ - set d : ℕ := FiniteDimensional.finrank ℝ E + set d : ℕ := Module.finrank ℝ E have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := fun r hr ↦ by refine (measure_mono <| hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_ diff --git a/Mathlib/Analysis/Convex/Normed.lean b/Mathlib/Analysis/Convex/Normed.lean index 2cb4a8b2db0d7..bfb9ac2e29cd3 100644 --- a/Mathlib/Analysis/Convex/Normed.lean +++ b/Mathlib/Analysis/Convex/Normed.lean @@ -27,7 +27,7 @@ We prove the following facts: variable {ι : Type*} {E P : Type*} -open AffineBasis FiniteDimensional Metric Set +open AffineBasis Module Metric Set open scoped Convex Pointwise Topology section SeminormedAddCommGroup diff --git a/Mathlib/Analysis/Convex/Radon.lean b/Mathlib/Analysis/Convex/Radon.lean index ee505ba41b251..f297649b6f470 100644 --- a/Mathlib/Analysis/Convex/Radon.lean +++ b/Mathlib/Analysis/Convex/Radon.lean @@ -62,7 +62,7 @@ theorem radon_partition {f : ι → E} (h : ¬ AffineIndependent 𝕜 f) : · linarith only [hI, hJI] · exact (mem_filter.mp hi').2.not_lt (mem_filter.mp hi).2 -open FiniteDimensional +open Module /-- Corner case for `helly_theorem'`. -/ private lemma helly_theorem_corner {F : ι → Set E} {s : Finset ι} diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 17917e748b4da..e7a99ac85a5d0 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -575,7 +575,7 @@ lemma _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) : variable [NormedAddCommGroup D] [MeasurableSpace D] -open MeasureTheory FiniteDimensional +open MeasureTheory Module /-- A measure `μ` has temperate growth if there is an `n : ℕ` such that `(1 + ‖x‖) ^ (- n)` is `μ`-integrable. -/ @@ -1036,7 +1036,7 @@ section Integration /-! ### Integration -/ -open Real Complex Filter MeasureTheory MeasureTheory.Measure FiniteDimensional +open Real Complex Filter MeasureTheory MeasureTheory.Measure Module variable [RCLike 𝕜] variable [NormedAddCommGroup D] [NormedSpace ℝ D] diff --git a/Mathlib/Analysis/Fourier/Inversion.lean b/Mathlib/Analysis/Fourier/Inversion.lean index cea8c2f5ade12..158aae8391b20 100644 --- a/Mathlib/Analysis/Fourier/Inversion.lean +++ b/Mathlib/Analysis/Fourier/Inversion.lean @@ -37,7 +37,7 @@ To check the concentration property of the middle factor and the fact that it ha rely on the explicit computation of the Fourier transform of Gaussians. -/ -open Filter MeasureTheory Complex FiniteDimensional Metric Real Bornology +open Filter MeasureTheory Complex Module Metric Real Bornology open scoped Topology FourierTransform RealInnerProductSpace Complex diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index 5b128034dec9b..1531edb4f4be0 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -45,7 +45,7 @@ equivalence to an inner-product space. noncomputable section -open MeasureTheory Filter Complex Set FiniteDimensional +open MeasureTheory Filter Complex Set Module open scoped Filter Topology Real ENNReal FourierTransform RealInnerProductSpace NNReal diff --git a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean index 6b402f751dabd..5e1e46a1e699c 100644 --- a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean +++ b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean @@ -349,7 +349,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux [Fintype ι] variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] -open FiniteDimensional +open Module /-- The constant factor occurring in the conclusion of `lintegral_pow_le_pow_lintegral_fderiv`. It only depends on `E`, `μ` and `p`. diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean index 29e41c81cd70d..13a75a6ea3529 100644 --- a/Mathlib/Analysis/InnerProductSpace/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean @@ -990,7 +990,7 @@ theorem exists_maximal_orthonormal {s : Set E} (hs : Orthonormal 𝕜 (Subtype.v · exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc · exact fun _ => Set.subset_sUnion_of_mem -open FiniteDimensional +open Module /-- A family of orthonormal vectors with the correct cardinality forms a basis. -/ def basisOfOrthonormalOfCardEqFinrank [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v) diff --git a/Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean b/Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean index 69889f1ed8e41..50173dd6a64c2 100644 --- a/Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean +++ b/Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean @@ -29,7 +29,7 @@ variable {E : Type*} [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup noncomputable section -open FiniteDimensional +open Module /-- If `E` is a finite dimensional space over `ℝ`, then `toEuclidean` is a continuous `ℝ`-linear equivalence between `E` and the Euclidean space of the same dimension. -/ diff --git a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean index a3c9277c121f4..b0351cdc69d46 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean @@ -35,7 +35,7 @@ and outputs a set of orthogonal vectors which have the same span. -/ -open Finset Submodule FiniteDimensional +open Finset Submodule Module variable (𝕜 : Type*) {E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] variable {ι : Type*} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι (· < ·)] diff --git a/Mathlib/Analysis/InnerProductSpace/Orientation.lean b/Mathlib/Analysis/InnerProductSpace/Orientation.lean index 60b27da658fe3..fb73168b5bab2 100644 --- a/Mathlib/Analysis/InnerProductSpace/Orientation.lean +++ b/Mathlib/Analysis/InnerProductSpace/Orientation.lean @@ -38,7 +38,7 @@ noncomputable section variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] -open FiniteDimensional +open Module open scoped RealInnerProductSpace diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean index 03d1f51b135c5..5fb4aa1c20293 100644 --- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean @@ -144,11 +144,11 @@ variable [Fintype ι] @[simp] theorem finrank_euclideanSpace : - FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by + Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by simp [EuclideanSpace, PiLp, WithLp] theorem finrank_euclideanSpace_fin {n : ℕ} : - FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp + Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp theorem EuclideanSpace.inner_eq_star_dotProduct (x y : EuclideanSpace 𝕜 ι) : ⟪x, y⟫ = Matrix.dotProduct (star <| WithLp.equiv _ _ x) (WithLp.equiv _ _ y) := @@ -669,7 +669,7 @@ theorem Complex.isometryOfOrthonormal_apply (v : OrthonormalBasis (Fin 2) ℝ F) end Complex -open FiniteDimensional +open Module /-! ### Matrix representation of an orthonormal basis with respect to another -/ @@ -792,7 +792,7 @@ theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq {ι : Type*} [F obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension have hιY : Fintype.card ι = Y.card := by refine card_ι.symm.trans ?_ - exact FiniteDimensional.finrank_eq_card_finset_basis b₀.toBasis + exact Module.finrank_eq_card_finset_basis b₀.toBasis have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict]) have hsv' : Set.InjOn v s := by rw [Set.injOn_iff_injective] @@ -840,7 +840,7 @@ irreducible_def DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) : (Σi, Fin (finrank 𝕜 (V i))) ≃ Fin n := let b := hV.collectedOrthonormalBasis hV' fun i => stdOrthonormalBasis 𝕜 (V i) - Fintype.equivFinOfCardEq <| (FiniteDimensional.finrank_eq_card_basis b.toBasis).symm.trans hn + Fintype.equivFinOfCardEq <| (Module.finrank_eq_card_basis b.toBasis).symm.trans hn /-- An `n`-dimensional `InnerProductSpace` equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by `Fin n` and subordinate to that direct sum. -/ @@ -885,7 +885,7 @@ section LinearIsometry variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] variable {S : Submodule 𝕜 V} {L : S →ₗᵢ[𝕜] V} -open FiniteDimensional +open Module /-- Let `S` be a subspace of a finite-dimensional complex inner product space `V`. A linear isometry mapping `S` into `V` can be extended to a full isometry of `V`. diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index dff8bfa3ecd3d..17223b1faf998 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1029,7 +1029,7 @@ theorem orthogonalProjection_isSymmetric [HasOrthogonalProjection K] : (K.subtypeL ∘L orthogonalProjection K : E →ₗ[𝕜] E).IsSymmetric := inner_orthogonalProjection_left_eq_right K -open FiniteDimensional +open Module /-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁` contained in it, the dimensions of `K₁` and the intersection of its @@ -1038,7 +1038,7 @@ theorem Submodule.finrank_add_inf_finrank_orthogonal {K₁ K₂ : Submodule 𝕜 [FiniteDimensional 𝕜 K₂] (h : K₁ ≤ K₂) : finrank 𝕜 K₁ + finrank 𝕜 (K₁ᗮ ⊓ K₂ : Submodule 𝕜 E) = finrank 𝕜 K₂ := by haveI : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h - haveI := proper_rclike 𝕜 K₁ + haveI := FiniteDimensional.proper_rclike 𝕜 K₁ have hd := Submodule.finrank_sup_add_finrank_inf_eq K₁ (K₁ᗮ ⊓ K₂) rw [← inf_assoc, (Submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot, Submodule.sup_orthogonal_inf_of_completeSpace h] at hd @@ -1270,7 +1270,7 @@ section OrthonormalBasis variable {v : Set E} -open FiniteDimensional Submodule Set +open Module Submodule Set /-- An orthonormal set in an `InnerProductSpace` is maximal, if and only if the orthogonal complement of its span is empty. -/ @@ -1341,7 +1341,7 @@ variable [FiniteDimensional 𝕜 E] is a basis. -/ theorem maximal_orthonormal_iff_basis_of_finiteDimensional (hv : Orthonormal 𝕜 ((↑) : v → E)) : (∀ u ⊇ v, Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ ∃ b : Basis v 𝕜 E, ⇑b = ((↑) : v → E) := by - haveI := proper_rclike 𝕜 (span 𝕜 v) + haveI := FiniteDimensional.proper_rclike 𝕜 (span 𝕜 v) rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv] rw [Submodule.orthogonal_eq_bot_iff] have hv_coe : range ((↑) : v → E) = v := by simp diff --git a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean index 68d1c7ecfc1b4..0f4bd55b7bae8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Spectrum.lean +++ b/Mathlib/Analysis/InnerProductSpace/Spectrum.lean @@ -184,7 +184,7 @@ end Version1 section Version2 -variable {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) +variable {n : ℕ} (hn : Module.finrank 𝕜 E = n) /-- A choice of orthonormal basis of eigenvectors for self-adjoint operator `T` on a finite-dimensional inner product space `E`. diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean index 1f3cbc87585d7..329dd441e2adc 100644 --- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -71,7 +71,7 @@ noncomputable section open scoped RealInnerProductSpace ComplexConjugate -open FiniteDimensional +open Module lemma FiniteDimensional.of_fact_finrank_eq_two {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (finrank K V = 2)] : FiniteDimensional K V := @@ -204,7 +204,7 @@ def rightAngleRotationAux₂ : E →ₗᵢ[ℝ] E := exact o.areaForm_le x (o.rightAngleRotationAux₁ x) · let K : Submodule ℝ E := ℝ ∙ x have : Nontrivial Kᗮ := by - apply @FiniteDimensional.nontrivial_of_finrank_pos ℝ + apply nontrivial_of_finrank_pos (R := ℝ) have : finrank ℝ K ≤ Finset.card {x} := by rw [← Set.toFinset_singleton] exact finrank_span_le_card ({x} : Set E) diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean index 4c55f7d09dafa..4735888f210dd 100644 --- a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean +++ b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean @@ -48,7 +48,7 @@ universe u v w x noncomputable section -open Set FiniteDimensional TopologicalSpace Filter Asymptotics Topology NNReal Metric +open Asymptotics Filter Module Metric Module NNReal Set TopologicalSpace Topology namespace LinearIsometry @@ -323,14 +323,14 @@ theorem Basis.exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) : instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] : SecondCountableTopology (E →L[𝕜] F) := by - set d := FiniteDimensional.finrank 𝕜 E + set d := Module.finrank 𝕜 E suffices ∀ ε > (0 : ℝ), ∃ n : (E →L[𝕜] F) → Fin d → ℕ, ∀ f g : E →L[𝕜] F, n f = n g → dist f g ≤ ε from Metric.secondCountable_of_countable_discretization fun ε ε_pos => ⟨Fin d → ℕ, by infer_instance, this ε ε_pos⟩ intro ε ε_pos obtain ⟨u : ℕ → F, hu : DenseRange u⟩ := exists_dense_seq F - let v := FiniteDimensional.finBasis 𝕜 E + let v := Module.finBasis 𝕜 E obtain ⟨C : ℝ, C_pos : 0 < C, hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖φ (v i)‖ ≤ M) → ‖φ‖ ≤ C * M⟩ := @@ -647,7 +647,7 @@ theorem summable_norm_iff {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ refine ⟨Summable.of_norm, fun hf ↦ ?_⟩ -- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ` suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by - obtain v := finBasis ℝ E + obtain v := Module.finBasis ℝ E set e := v.equivFunL have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf) refine .of_norm_bounded _ (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_ diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean index ce018727e6c0f..b158eee9c860d 100644 --- a/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean +++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean @@ -107,7 +107,7 @@ theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : p →L[𝕜] 𝕜) : _ = ‖f‖ := by rw [reCLM_norm, one_mul] · exact f.opNorm_le_bound g.extendTo𝕜.opNorm_nonneg fun x => h x ▸ g.extendTo𝕜.le_opNorm x -open FiniteDimensional +open Module /-- Corollary of the **Hahn-Banach theorem**: if `f : p → F` is a continuous linear map from a submodule of a normed space `E` over `𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`, @@ -120,7 +120,7 @@ lemma ContinuousLinearMap.exist_extension_of_finiteDimensional_range {p : Submod (f : p →L[𝕜] F) [FiniteDimensional 𝕜 (LinearMap.range f)] : ∃ g : E →L[𝕜] F, f = g.comp p.subtypeL := by letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜 - set b := finBasis 𝕜 (LinearMap.range f) + set b := Module.finBasis 𝕜 (LinearMap.range f) set e := b.equivFunL set fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict _ <| LinearMap.mem_range_self _) diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean index ea572b4ce3c4e..89db8290e3687 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean @@ -332,18 +332,18 @@ theorem integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace theorem integral_cexp_neg_mul_sq_norm_add (hb : 0 < b.re) (c : ℂ) (w : V) : ∫ v : V, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) = - (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b)) := by + (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b)) := by let e := (stdOrthonormalBasis ℝ V).repr.symm rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding] convert integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace hb c (e.symm w) <;> simp [LinearIsometryEquiv.inner_map_eq_flip] theorem integral_cexp_neg_mul_sq_norm (hb : 0 < b.re) : - ∫ v : V, cexp (- b * ‖v‖^2) = (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) := by + ∫ v : V, cexp (- b * ‖v‖^2) = (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) := by simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V) theorem integral_rexp_neg_mul_sq_norm {b : ℝ} (hb : 0 < b) : - ∫ v : V, rexp (- b * ‖v‖^2) = (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℝ) := by + ∫ v : V, rexp (- b * ‖v‖^2) = (π / b) ^ (Module.finrank ℝ V / 2 : ℝ) := by rw [← ofReal_inj] convert integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V) · change ofRealLI (∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2) @@ -354,7 +354,7 @@ theorem integral_rexp_neg_mul_sq_norm {b : ℝ} (hb : 0 < b) : theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w : V) : 𝓕 (fun v ↦ cexp (- b * ‖v‖^2 + 2 * π * Complex.I * ⟪x, v⟫)) w = - (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖x - w‖ ^ 2 / b) := by + (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖x - w‖ ^ 2 / b) := by simp only [neg_mul, fourierIntegral_eq', ofReal_neg, ofReal_mul, ofReal_ofNat, smul_eq_mul, ← Complex.exp_add, real_inner_comm w] convert integral_cexp_neg_mul_sq_norm_add hb (2 * π * Complex.I) (x - w) using 3 with v @@ -367,7 +367,7 @@ theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w theorem _root_.fourierIntegral_gaussian_innerProductSpace (hb : 0 < b.re) (w : V) : 𝓕 (fun v ↦ cexp (- b * ‖v‖^2)) w = - (π / b) ^ (FiniteDimensional.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖^2 / b) := by + (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖^2 / b) := by simpa using fourierIntegral_gaussian_innerProductSpace' hb 0 w end InnerProductSpace diff --git a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean index 86a45e8436078..5b9cbab201ab2 100644 --- a/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean +++ b/Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean @@ -27,7 +27,7 @@ noncomputable section open scoped NNReal Filter Topology ENNReal -open Asymptotics Filter Set Real MeasureTheory FiniteDimensional +open Asymptotics Filter Set Real MeasureTheory Module variable {E : Type*} [NormedAddCommGroup E] diff --git a/Mathlib/CategoryTheory/Preadditive/Schur.lean b/Mathlib/CategoryTheory/Preadditive/Schur.lean index 407e246e350e0..2fd3b980f6f59 100644 --- a/Mathlib/CategoryTheory/Preadditive/Schur.lean +++ b/Mathlib/CategoryTheory/Preadditive/Schur.lean @@ -70,7 +70,7 @@ noncomputable instance [HasKernels C] {X : C} [Simple X] : DivisionRing (End X) qsmul := _ qsmul_def := fun q a => rfl -open FiniteDimensional +open Module section diff --git a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean index 40f0ebf38db1e..e609a7dee3f0e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean @@ -189,8 +189,8 @@ end /-- The number of connected components in `G` is the dimension of the nullspace its Laplacian. -/ theorem card_ConnectedComponent_eq_rank_ker_lapMatrix : Fintype.card G.ConnectedComponent = - FiniteDimensional.finrank ℝ (LinearMap.ker (Matrix.toLin' (G.lapMatrix ℝ))) := by + Module.finrank ℝ (LinearMap.ker (Matrix.toLin' (G.lapMatrix ℝ))) := by classical - rw [FiniteDimensional.finrank_eq_card_basis (lapMatrix_ker_basis G)] + rw [Module.finrank_eq_card_basis (lapMatrix_ker_basis G)] end SimpleGraph diff --git a/Mathlib/Data/Complex/FiniteDimensional.lean b/Mathlib/Data/Complex/FiniteDimensional.lean index 5fbde35674c53..f989ee2a1847c 100644 --- a/Mathlib/Data/Complex/FiniteDimensional.lean +++ b/Mathlib/Data/Complex/FiniteDimensional.lean @@ -15,12 +15,11 @@ This file contains the `FiniteDimensional ℝ ℂ` instance, as well as some res (`finrank` and `Module.rank`). -/ -open FiniteDimensional +open Module namespace Complex -instance : FiniteDimensional ℝ ℂ := - of_fintype_basis basisOneI +instance : FiniteDimensional ℝ ℂ := .of_fintype_basis basisOneI @[simp] theorem finrank_real_complex : finrank ℝ ℂ = 2 := by @@ -50,8 +49,8 @@ theorem rank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] : simp only [Cardinal.lift_id'] theorem finrank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] : - FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E := by - rw [← FiniteDimensional.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex] + Module.finrank ℝ E = 2 * Module.finrank ℂ E := by + rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex] section Rational diff --git a/Mathlib/Data/Matrix/Rank.lean b/Mathlib/Data/Matrix/Rank.lean index d272ff6eb228a..13db0d03e2bc9 100644 --- a/Mathlib/Data/Matrix/Rank.lean +++ b/Mathlib/Data/Matrix/Rank.lean @@ -26,7 +26,7 @@ open Matrix namespace Matrix -open FiniteDimensional +open Module variable {l m n o R : Type*} [Fintype n] [Fintype o] @@ -168,7 +168,7 @@ variable [Field R] /-- The rank of a diagnonal matrix is the count of non-zero elements on its main diagonal -/ theorem rank_diagonal [Fintype m] [DecidableEq m] [DecidableEq R] (w : m → R) : (diagonal w).rank = Fintype.card {i // (w i) ≠ 0} := by - rw [Matrix.rank, ← Matrix.toLin'_apply', FiniteDimensional.finrank, ← LinearMap.rank, + rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank, LinearMap.rank_diagonal, Cardinal.toNat_natCast] end Field @@ -278,7 +278,7 @@ lemma rank_add_rank_le_card_of_mul_eq_zero [Field R] [Finite l] [Fintype m] let en : Basis n R (n → R) := Pi.basisFun R n rw [Matrix.rank_eq_finrank_range_toLin A el em, Matrix.rank_eq_finrank_range_toLin B em en, - ← FiniteDimensional.finrank_fintype_fun_eq_card R, + ← Module.finrank_fintype_fun_eq_card R, ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A), add_le_add_iff_left] apply Submodule.finrank_mono diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index e4701e89934ea..c83073349810a 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -28,7 +28,7 @@ For example, `Algebra.adjoin K {x}` might not include `x⁻¹`. - `F⟮α⟯`: adjoin a single element `α` to `F` (in scope `IntermediateField`). -/ -open FiniteDimensional Polynomial +open Module Polynomial namespace IntermediateField @@ -872,7 +872,7 @@ theorem adjoin_natCast (n : ℕ) : F⟮(n : E)⟯ = ⊥ := section AdjoinRank -open FiniteDimensional Module +open Module Module variable {K L : IntermediateField F E} @@ -1043,7 +1043,7 @@ theorem isAlgebraic_adjoin_simple {x : L} (hx : IsIntegral K x) : Algebra.IsAlge have := adjoin.finiteDimensional hx; Algebra.IsAlgebraic.of_finite K K⟮x⟯ theorem adjoin.finrank {x : L} (hx : IsIntegral K x) : - FiniteDimensional.finrank K K⟮x⟯ = (minpoly K x).natDegree := by + Module.finrank K K⟮x⟯ = (minpoly K x).natDegree := by rw [PowerBasis.finrank (adjoin.powerBasis hx : _)] rfl @@ -1117,11 +1117,10 @@ theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] : /-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the minimal polynomial of `x` over `K` divides `[L : K]`.-/ theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) : - (minpoly K x).natDegree ∣ FiniteDimensional.finrank K L := by + (minpoly K x).natDegree ∣ finrank K L := by rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx] - use FiniteDimensional.finrank K⟮x⟯ L - rw [eq_comm, mul_comm] - exact FiniteDimensional.finrank_mul_finrank _ _ _ + use finrank K⟮x⟯ L + rw [mul_comm, finrank_mul_finrank] -- TODO: generalize to `Sort` /-- A compositum of algebraic extensions is algebraic -/ @@ -1178,7 +1177,7 @@ theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : IsSeparable F exact h_sep -- Apparently `K⟮root f⟯ →+* K⟮root f⟯` is expensive to unify during instance synthesis. -open FiniteDimensional AdjoinRoot in +open Module AdjoinRoot in /-- Let `f, g` be monic polynomials over `K`. If `f` is irreducible, and `g(x) - α` is irreducible in `K⟮α⟯` with `α` a root of `f`, then `f(g(x))` is irreducible. -/ theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g.Monic) @@ -1226,7 +1225,7 @@ theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g rw [← finrank_top', ← this, adjoin.finrank] exact IsIntegral.of_finite _ _ · simp [← key₂] - have := FiniteDimensional.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx + have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this end AdjoinIntegralElement diff --git a/Mathlib/FieldTheory/Cardinality.lean b/Mathlib/FieldTheory/Cardinality.lean index 8a0482682912f..045db9322dcbf 100644 --- a/Mathlib/FieldTheory/Cardinality.lean +++ b/Mathlib/FieldTheory/Cardinality.lean @@ -43,8 +43,8 @@ theorem Fintype.isPrimePow_card_of_field {α} [Fintype α] [Field α] : IsPrimeP let b := IsNoetherian.finsetBasis (ZMod p) α rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff] · exact hp.1.isPrimePow - rw [← FiniteDimensional.finrank_eq_card_basis b] - exact FiniteDimensional.finrank_pos.ne' + rw [← Module.finrank_eq_card_basis b] + exact Module.finrank_pos.ne' /-- A `Fintype` can be given a field structure iff its cardinality is a prime power. -/ theorem Fintype.nonempty_field_iff {α} [Fintype α] : Nonempty (Field α) ↔ IsPrimePow ‖α‖ := by diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean index 6b5c4835a87c6..715387ba0669b 100644 --- a/Mathlib/FieldTheory/Finite/Basic.lean +++ b/Mathlib/FieldTheory/Finite/Basic.lean @@ -455,9 +455,9 @@ variable {V : Type*} [Fintype K] [DivisionRing K] [AddCommGroup V] [Module K V] -- should this go in a namespace? -- finite_dimensional would be natural, -- but we don't assume it... -theorem card_eq_pow_finrank [Fintype V] : Fintype.card V = q ^ FiniteDimensional.finrank K V := by +theorem card_eq_pow_finrank [Fintype V] : Fintype.card V = q ^ Module.finrank K V := by let b := IsNoetherian.finsetBasis K V - rw [Module.card_fintype b, ← FiniteDimensional.finrank_eq_card_basis b] + rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b] end diff --git a/Mathlib/FieldTheory/Finite/GaloisField.lean b/Mathlib/FieldTheory/Finite/GaloisField.lean index e03d1331f1020..89b627d0328c8 100644 --- a/Mathlib/FieldTheory/Finite/GaloisField.lean +++ b/Mathlib/FieldTheory/Finite/GaloisField.lean @@ -88,7 +88,7 @@ instance : Fintype (GaloisField p n) := by dsimp only [GaloisField] exact FiniteDimensional.fintypeOfFintype (ZMod p) (GaloisField p n) -theorem finrank {n} (h : n ≠ 0) : FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n := by +theorem finrank {n} (h : n ≠ 0) : Module.finrank (ZMod p) (GaloisField p n) = n := by set g_poly := (X ^ p ^ n - X : (ZMod p)[X]) have hp : 1 < p := h_prime.out.one_lt have aux : g_poly ≠ 0 := FiniteField.X_pow_card_pow_sub_X_ne_zero _ h hp @@ -139,7 +139,7 @@ theorem finrank {n} (h : n ≠ 0) : FiniteDimensional.finrank (ZMod p) (GaloisFi theorem card (h : n ≠ 0) : Fintype.card (GaloisField p n) = p ^ n := by let b := IsNoetherian.finsetBasis (ZMod p) (GaloisField p n) - rw [Module.card_fintype b, ← FiniteDimensional.finrank_eq_card_basis b, ZMod.card, finrank p h] + rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b, ZMod.card, finrank p h] theorem splits_zmod_X_pow_sub_X : Splits (RingHom.id (ZMod p)) (X ^ p - X) := by have hp : 1 < p := h_prime.out.one_lt diff --git a/Mathlib/FieldTheory/Finite/Polynomial.lean b/Mathlib/FieldTheory/Finite/Polynomial.lean index 8207de7d06c14..00e92545eba5b 100644 --- a/Mathlib/FieldTheory/Finite/Polynomial.lean +++ b/Mathlib/FieldTheory/Finite/Polynomial.lean @@ -215,8 +215,8 @@ instance [Finite σ] : FiniteDimensional K (R σ K) := by simpa only [rank_R] using Cardinal.nat_lt_aleph0 (Fintype.card (σ → K))) open Classical in -theorem finrank_R [Fintype σ] : FiniteDimensional.finrank K (R σ K) = Fintype.card (σ → K) := - FiniteDimensional.finrank_eq_of_rank_eq (rank_R σ K) +theorem finrank_R [Fintype σ] : Module.finrank K (R σ K) = Fintype.card (σ → K) := + Module.finrank_eq_of_rank_eq (rank_R σ K) -- Porting note: was `(evalᵢ σ K).range`. theorem range_evalᵢ [Finite σ] : range (evalᵢ σ K) = ⊤ := by @@ -228,7 +228,7 @@ theorem ker_evalₗ [Finite σ] : ker (evalᵢ σ K) = ⊥ := by cases nonempty_fintype σ refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K) classical - rw [FiniteDimensional.finrank_fintype_fun_eq_card, finrank_R] + rw [Module.finrank_fintype_fun_eq_card, finrank_R] theorem eq_zero_of_eval_eq_zero [Finite σ] (p : MvPolynomial σ K) (h : ∀ v : σ → K, eval v p = 0) (hp : p ∈ restrictDegree σ K (Fintype.card K - 1)) : p = 0 := diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean index bf86498f3027a..965f23a35eefe 100644 --- a/Mathlib/FieldTheory/Fixed.lean +++ b/Mathlib/FieldTheory/Fixed.lean @@ -30,7 +30,7 @@ element of `G`, where `G` is a group that acts on `F`. noncomputable section -open MulAction Finset FiniteDimensional +open MulAction Finset Module universe u v w diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean index 56ce629fc2bea..3f571ef51fa06 100644 --- a/Mathlib/FieldTheory/Galois/Basic.lean +++ b/Mathlib/FieldTheory/Galois/Basic.lean @@ -35,7 +35,7 @@ Together, these two results prove the Galois correspondence. open scoped Polynomial IntermediateField -open FiniteDimensional AlgEquiv +open Module AlgEquiv section diff --git a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean index 99eab922d6a3d..55ecc96148306 100644 --- a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean +++ b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean @@ -13,7 +13,7 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition # Results on finite dimensionality and algebraicity of intermediate fields. -/ -open FiniteDimensional +open Module variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} @@ -24,11 +24,8 @@ section FiniteDimensional variable (F E : IntermediateField K L) -instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F := - left K F L - -instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L := - right K F L +instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F := .left K F L +instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L := .right K F L @[simp] theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F := diff --git a/Mathlib/FieldTheory/IsPerfectClosure.lean b/Mathlib/FieldTheory/IsPerfectClosure.lean index 70d3708472eb5..743199124c340 100644 --- a/Mathlib/FieldTheory/IsPerfectClosure.lean +++ b/Mathlib/FieldTheory/IsPerfectClosure.lean @@ -60,7 +60,7 @@ perfect ring, perfect closure, purely inseparable -/ -open FiniteDimensional Polynomial IntermediateField Field +open Module Polynomial IntermediateField Field noncomputable section diff --git a/Mathlib/FieldTheory/KummerExtension.lean b/Mathlib/FieldTheory/KummerExtension.lean index 4be37a02bc718..939bc161ec3f8 100644 --- a/Mathlib/FieldTheory/KummerExtension.lean +++ b/Mathlib/FieldTheory/KummerExtension.lean @@ -530,7 +530,7 @@ lemma isGalois_of_isSplittingField_X_pow_sub_C : IsGalois K L := IsGalois.of_separable_splitting_field (separable_X_pow_sub_C_of_irreducible hζ a H) include hζ H in -lemma finrank_of_isSplittingField_X_pow_sub_C : FiniteDimensional.finrank K L = n := by +lemma finrank_of_isSplittingField_X_pow_sub_C : Module.finrank K L = n := by have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a) have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H) @@ -545,9 +545,9 @@ end IsSplittingField section IsCyclic variable {L} [Field L] [Algebra K L] [FiniteDimensional K L] -variable (hK : (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty) +variable (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) -open FiniteDimensional +open Module variable (K L) include hK in @@ -623,7 +623,7 @@ lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top end IsCyclic -open FiniteDimensional in +open Module in /-- Suppose `L/K` is a finite extension of dimension `n`, and `K` contains all `n`-th roots of unity. Then `L/K` is cyclic iff @@ -631,7 +631,7 @@ Then `L/K` is cyclic iff `L = K[α]` for some `αⁿ ∈ K`. -/ lemma isCyclic_tfae (K L) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] - (hK : (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty) : + (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) : List.TFAE [ IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L), ∃ a : K, Irreducible (X ^ (finrank K L) - C a) ∧ diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean index b62efc1339b8a..3a33353b9af98 100644 --- a/Mathlib/FieldTheory/Minpoly/Field.lean +++ b/Mathlib/FieldTheory/Minpoly/Field.lean @@ -162,7 +162,7 @@ variable (F E K : Type*) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F -- though it isn't very computable in practice (since neither `finrank` nor `finBasis` are). /-- Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x -/ def rootsOfMinPolyPiType (φ : E →ₐ[F] K) - (x : range (FiniteDimensional.finBasis F E : _ → E)) : + (x : range (Module.finBasis F E : _ → E)) : { l : K // l ∈ (minpoly F x.1).aroots K } := ⟨φ x, by rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val), @@ -173,14 +173,14 @@ theorem aux_inj_roots_of_min_poly : Injective (rootsOfMinPolyPiType F E K) := by -- needs explicit coercion on the RHS suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢ rw [funext_iff] at h - exact LinearMap.ext_on (FiniteDimensional.finBasis F E).span_eq fun e he => + exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he => Subtype.ext_iff.mp (h ⟨e, he⟩) /-- Given field extensions `E/F` and `K/F`, with `E/F` finite, there are finitely many `F`-algebra homomorphisms `E →ₐ[K] K`. -/ noncomputable instance AlgHom.fintype : Fintype (E →ₐ[F] K) := @Fintype.ofInjective _ _ - (Fintype.subtypeProd (finite_range (FiniteDimensional.finBasis F E)) fun e => + (Fintype.subtypeProd (finite_range (Module.finBasis F E)) fun e => (minpoly F e).aroots K) _ (aux_inj_roots_of_min_poly F E K) diff --git a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean index c327e135c3ddd..fae1bec1703c0 100644 --- a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean +++ b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean @@ -20,7 +20,7 @@ See `traceForm_dualBasis_powerBasis_eq`. - `span_coeff_minpolyDiv`: The coefficients of `minpolyDiv` spans `R`. -/ -open Polynomial FiniteDimensional +open Polynomial Module variable (R K) {L S} [CommRing R] [Field K] [Field L] [CommRing S] [Algebra R S] [Algebra K L] variable (x : S) diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean index 003d87b0e80d0..ef2d383b8d52b 100644 --- a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean +++ b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean @@ -41,7 +41,7 @@ noncomputable section open scoped Polynomial -open FiniteDimensional +open Module namespace Polynomial @@ -384,10 +384,10 @@ theorem prime_degree_dvd_card [CharZero F] (p_irr : Irreducible p) (p_deg : p.na let α : p.SplittingField := rootOfSplits (algebraMap F p.SplittingField) (SplittingField.splits p) hp have hα : IsIntegral F α := .of_finite F α - use FiniteDimensional.finrank F⟮α⟯ p.SplittingField + use Module.finrank F⟮α⟯ p.SplittingField suffices (minpoly F α).natDegree = p.natDegree by letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup - rw [← FiniteDimensional.finrank_mul_finrank F F⟮α⟯ p.SplittingField, + rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField, IntermediateField.adjoin.finrank hα, this] suffices minpoly F α ∣ p by have key := (minpoly.irreducible hα).dvd_symm p_irr this diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index 65b6d1707f19d..da215b5d8dbf4 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -36,7 +36,7 @@ exists_adjoin_simple_eq_top noncomputable section -open FiniteDimensional Polynomial IntermediateField +open Module Polynomial IntermediateField namespace Field @@ -63,7 +63,7 @@ theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α /-- Primitive element theorem for finite dimensional extension of a finite field. -/ theorem exists_primitive_element_of_finite_bot [Finite F] [FiniteDimensional F E] : ∃ α : E, F⟮α⟯ = ⊤ := - haveI : Finite E := finite_of_finite F E + haveI : Finite E := FiniteDimensional.finite_of_finite F E exists_primitive_element_of_finite_top F E end PrimitiveElementFinite @@ -367,7 +367,7 @@ section iff namespace Field -open FiniteDimensional IntermediateField Polynomial Algebra Set +open Module IntermediateField Polynomial Algebra Set variable (F : Type*) {E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] diff --git a/Mathlib/FieldTheory/PurelyInseparable.lean b/Mathlib/FieldTheory/PurelyInseparable.lean index f8b347c9bf68a..c880a81782d7f 100644 --- a/Mathlib/FieldTheory/PurelyInseparable.lean +++ b/Mathlib/FieldTheory/PurelyInseparable.lean @@ -127,7 +127,7 @@ separable degree, degree, separable closure, purely inseparable -/ -open FiniteDimensional Polynomial IntermediateField Field Finsupp +open Module Polynomial IntermediateField Field Finsupp noncomputable section @@ -756,7 +756,7 @@ private theorem LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable have h' := h.coe_range let ι' := h'.extend (Set.range v).subset_univ let b : Basis ι' F E := Basis.extend h' - letI : Fintype ι' := fintypeBasisIndex b + letI : Fintype ι' := FiniteDimensional.fintypeBasisIndex b have H := linearIndependent_of_top_le_span_of_card_eq_finrank (span_map_pow_expChar_pow_eq_top_of_isSeparable q n b.span_eq).ge (finrank_eq_card_basis b).symm diff --git a/Mathlib/FieldTheory/SeparableClosure.lean b/Mathlib/FieldTheory/SeparableClosure.lean index 596db72fdf6cd..68110800b109d 100644 --- a/Mathlib/FieldTheory/SeparableClosure.lean +++ b/Mathlib/FieldTheory/SeparableClosure.lean @@ -59,7 +59,7 @@ separable degree, degree, separable closure -/ -open FiniteDimensional Polynomial IntermediateField Field +open Module Polynomial IntermediateField Field noncomputable section diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean index 3bac952cdb9f8..6ebcf74215644 100644 --- a/Mathlib/FieldTheory/SeparableDegree.lean +++ b/Mathlib/FieldTheory/SeparableDegree.lean @@ -67,7 +67,7 @@ This file contains basics about the separable degree of a field extension. if `K / E / F` is a field extension tower, such that `K / E` is algebraic, then there is a non-canonical bijection `Field.Emb F E × Field.Emb E K ≃ Field.Emb F K`. In particular, the separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$ - (see also `FiniteDimensional.finrank_mul_finrank`). + (see also `Module.finrank_mul_finrank`). - `Polynomial.natSepDegree_le_natDegree`: the separable degree of a polynomial is smaller than its degree. @@ -118,7 +118,7 @@ separable degree, degree, polynomial -/ -open FiniteDimensional Polynomial IntermediateField Field +open Module Polynomial IntermediateField Field noncomputable section @@ -246,7 +246,7 @@ def embProdEmbOfIsAlgebraic [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgeb /-- If `K / E / F` is a field extension tower, such that `K / E` is algebraic, then their separable degrees satisfy the tower law -$[E:F]_s [K:E]_s = [K:F]_s$. See also `FiniteDimensional.finrank_mul_finrank`. -/ +$[E:F]_s [K:E]_s = [K:F]_s$. See also `Module.finrank_mul_finrank`. -/ theorem finSepDegree_mul_finSepDegree_of_isAlgebraic [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K] : finSepDegree F E * finSepDegree E K = finSepDegree F K := by @@ -701,7 +701,7 @@ theorem finSepDegree_dvd_finrank : finSepDegree F E ∣ finrank F E := by set M := L⟮x⟯ have := Algebra.IsAlgebraic.of_finite L M rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M, - FiniteDimensional.finrank_mul_finrank F L M] at hdvd + Module.finrank_mul_finrank F L M] at hdvd rw [finrank_of_infinite_dimensional hfd] exact dvd_zero _ @@ -735,7 +735,7 @@ theorem finSepDegree_eq_finrank_of_isSeparable [Algebra.IsSeparable F E] : set M := L⟮x⟯ have := Algebra.IsAlgebraic.of_finite L M rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M, - FiniteDimensional.finrank_mul_finrank F L M] at heq + Module.finrank_mul_finrank F L M] at heq alias Algebra.IsSeparable.finSepDegree_eq := finSepDegree_eq_finrank_of_isSeparable @@ -749,7 +749,7 @@ theorem finSepDegree_eq_finrank_iff [FiniteDimensional F E] : (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_lt fun h ↦ ?_ have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.size_pos' rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E, - FiniteDimensional.finrank_mul_finrank F F⟮x⟯ E] at this + Module.finrank_mul_finrank F F⟮x⟯ E] at this linarith only [heq, this]⟩, fun _ ↦ finSepDegree_eq_finrank_of_isSeparable F E⟩ end Field @@ -796,7 +796,7 @@ theorem IsSeparable.of_algebra_isSeparable_of_isSeparable [Algebra E K] [IsScala have := finSepDegree_mul_finSepDegree_of_isAlgebraic F E' E'⟮x⟯ rw [finSepDegree_eq_finrank_of_isSeparable F E', finSepDegree_eq_finrank_of_isSeparable E' E'⟮x⟯, - FiniteDimensional.finrank_mul_finrank F E' E'⟮x⟯, + Module.finrank_mul_finrank F E' E'⟮x⟯, eq_comm, finSepDegree_eq_finrank_iff F E'⟮x⟯] at this change Algebra.IsSeparable F (restrictScalars F E'⟮x⟯) at this exact isSeparable_of_mem_isSeparable F K hx diff --git a/Mathlib/FieldTheory/Tower.lean b/Mathlib/FieldTheory/Tower.lean index 4a4720b3cb6aa..297650824b8be 100644 --- a/Mathlib/FieldTheory/Tower.lean +++ b/Mathlib/FieldTheory/Tower.lean @@ -15,7 +15,7 @@ We prove that given `IsScalarTower F K A`, if `A` is finite as a module over `F` In particular these conditions hold when `A`, `F`, and `K` are fields. -The formulas for the dimensions are given elsewhere by `FiniteDimensional.finrank_mul_finrank`. +The formulas for the dimensions are given elsewhere by `Module.finrank_mul_finrank`. ## Tags diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean index 40018bcc026e4..6e6e991b9b0b4 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean @@ -22,7 +22,7 @@ This file defines oriented angles in Euclidean affine spaces. noncomputable section -open FiniteDimensional Complex +open Module Complex open scoped Affine EuclideanGeometry Real RealInnerProductSpace ComplexConjugate diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index fb641332e085a..3f2938cdce408 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -31,7 +31,7 @@ modulo `2 * π` as equalities of `(2 : ℤ) • θ`. noncomputable section -open FiniteDimensional Complex +open Module Complex open scoped Real RealInnerProductSpace ComplexConjugate diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean index d634919578060..8ca1f21c9b812 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean @@ -25,7 +25,7 @@ open scoped RealInnerProductSpace namespace Orientation -open FiniteDimensional +open Module variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] variable [hd2 : Fact (finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) @@ -519,7 +519,7 @@ end Orientation namespace EuclideanGeometry -open FiniteDimensional +open Module variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean index 7f40cc129de8e..734899c867f50 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean @@ -20,7 +20,7 @@ This file defines rotations by oriented angles in real inner product spaces. noncomputable section -open FiniteDimensional Complex +open Module Complex open scoped Real RealInnerProductSpace ComplexConjugate @@ -101,8 +101,7 @@ theorem rotation_eq_matrix_toLin (θ : Real.Angle) {x : V} (hx : x ≠ 0) : /-- The determinant of `rotation` (as a linear map) is equal to `1`. -/ @[simp] theorem det_rotation (θ : Real.Angle) : LinearMap.det (o.rotation θ).toLinearMap = 1 := by - haveI : Nontrivial V := - FiniteDimensional.nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _) + haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _) obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V) rw [o.rotation_eq_matrix_toLin θ hx] simpa [sq] using θ.cos_sq_add_sin_sq @@ -333,8 +332,7 @@ theorem oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {x y : V} (θ : Real.Angle theorem exists_linearIsometryEquiv_eq_of_det_pos {f : V ≃ₗᵢ[ℝ] V} (hd : 0 < LinearMap.det (f.toLinearEquiv : V →ₗ[ℝ] V)) : ∃ θ : Real.Angle, f = o.rotation θ := by - haveI : Nontrivial V := - FiniteDimensional.nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _) + haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _) obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V) use o.oangle x (f x) apply LinearIsometryEquiv.toLinearEquiv_injective diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean index dd2a20922dbdb..17315a1b24430 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean @@ -16,7 +16,7 @@ This file proves results about angles in circles and spheres. noncomputable section -open FiniteDimensional Complex +open Module Complex open scoped EuclideanGeometry Real RealInnerProductSpace ComplexConjugate diff --git a/Mathlib/Geometry/Euclidean/Basic.lean b/Mathlib/Geometry/Euclidean/Basic.lean index 3ac078670754f..55b07f87b916c 100644 --- a/Mathlib/Geometry/Euclidean/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Basic.lean @@ -124,7 +124,7 @@ theorem dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) mul_div_assoc] norm_num -open AffineSubspace FiniteDimensional +open AffineSubspace Module /-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at most two points `p₁` `p₂` in a two-dimensional subspace containing those points @@ -150,7 +150,7 @@ theorem eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {s : AffineSubspace · rw [real_inner_comm] exact ho have hbs : Submodule.span ℝ (Set.range b) = s.direction := by - refine eq_of_le_of_finrank_eq ?_ ?_ + refine Submodule.eq_of_le_of_finrank_eq ?_ ?_ · rw [Submodule.span_le, Set.range_subset_iff] intro i fin_cases i diff --git a/Mathlib/Geometry/Euclidean/Circumcenter.lean b/Mathlib/Geometry/Euclidean/Circumcenter.lean index ed19fa6831d20..ab715d6d83899 100644 --- a/Mathlib/Geometry/Euclidean/Circumcenter.lean +++ b/Mathlib/Geometry/Euclidean/Circumcenter.lean @@ -667,7 +667,7 @@ end Affine namespace EuclideanGeometry -open Affine AffineSubspace FiniteDimensional +open Affine AffineSubspace Module variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] diff --git a/Mathlib/Geometry/Euclidean/MongePoint.lean b/Mathlib/Geometry/Euclidean/MongePoint.lean index 6343ce224c3da..fbf488bef44b3 100644 --- a/Mathlib/Geometry/Euclidean/MongePoint.lean +++ b/Mathlib/Geometry/Euclidean/MongePoint.lean @@ -344,7 +344,7 @@ theorem vectorSpan_isOrtho_altitude_direction {n : ℕ} (s : Simplex ℝ P (n + rw [direction_altitude] exact (Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left -open FiniteDimensional +open Module /-- An altitude is finite-dimensional. -/ instance finiteDimensional_direction_altitude {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : @@ -392,7 +392,7 @@ theorem affineSpan_pair_eq_altitude_iff {n : ℕ} (s : Simplex ℝ P (n + 1)) (i rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _), Set.insert_diff_of_mem _ (Set.mem_singleton _), Set.diff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton] - refine eq_of_le_of_finrank_eq ?_ ?_ + refine Submodule.eq_of_le_of_finrank_eq ?_ ?_ · rw [Submodule.span_le] simpa using h · rw [finrank_direction_altitude, finrank_span_set_eq_card] @@ -404,7 +404,7 @@ end Simplex namespace Triangle -open EuclideanGeometry Finset Simplex AffineSubspace FiniteDimensional +open EuclideanGeometry Finset Simplex AffineSubspace Module variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] @@ -548,7 +548,8 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P} have he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points) := by refine ext_of_direction_eq ?_ ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩ - refine eq_of_le_of_finrank_eq (direction_le (spanPoints_subset_coe_of_subset_coe ?_)) ?_ + refine Submodule.eq_of_le_of_finrank_eq (direction_le (spanPoints_subset_coe_of_subset_coe ?_)) + ?_ · have hu : (Finset.univ : Finset (Fin 3)) = {j₁, j₂, j₃} := by clear h₁ h₂ h₃ -- Porting note (#11043): was `decide!` @@ -602,7 +603,7 @@ end Affine namespace EuclideanGeometry -open Affine AffineSubspace FiniteDimensional +open Affine AffineSubspace Module variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] @@ -706,7 +707,7 @@ theorem affineSpan_of_orthocentricSystem {s : Set P} (ho : OrthocentricSystem s) ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩ have hfd : FiniteDimensional ℝ (affineSpan ℝ s).direction := by rw [hs]; infer_instance haveI := hfd - refine eq_of_le_of_finrank_eq (direction_le (affineSpan_mono ℝ hps)) ?_ + refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_mono ℝ hps)) ?_ rw [hs, direction_affineSpan, direction_affineSpan, ha.finrank_vectorSpan (Fintype.card_fin _), t.independent.finrank_vectorSpan (Fintype.card_fin _)] diff --git a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean index 20d5711b81e4d..6c5067aad4c23 100644 --- a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean @@ -33,7 +33,7 @@ namespace EuclideanGeometry variable {V : Type*} (P : Type*) -open FiniteDimensional +open Module /-- A `Sphere P` bundles a `center` and `radius`. This definition does not require the radius to be positive; that should be given as a hypothesis to lemmas that require it. -/ diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index 5a28ab76286ee..9e2ab6a89582d 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/Mathlib/Geometry/Euclidean/Triangle.lean @@ -295,7 +295,7 @@ theorem angle_add_angle_add_angle_eq_pi {p1 p2 p3 : P} (h2 : p2 ≠ p1) (h3 : p3 /-- The **sum of the angles of a triangle** (possibly degenerate, where the triangle is a line), oriented angles at point. -/ theorem oangle_add_oangle_add_oangle_eq_pi [Module.Oriented ℝ V (Fin 2)] - [Fact (FiniteDimensional.finrank ℝ V = 2)] {p1 p2 p3 : P} (h21 : p2 ≠ p1) (h32 : p3 ≠ p2) + [Fact (Module.finrank ℝ V = 2)] {p1 p2 p3 : P} (h21 : p2 ≠ p1) (h32 : p3 ≠ p2) (h13 : p1 ≠ p3) : ∡ p1 p2 p3 + ∡ p2 p3 p1 + ∡ p3 p1 p2 = π := by simpa only [neg_vsub_eq_vsub_rev] using positiveOrientation.oangle_add_cyc3_neg_left (vsub_ne_zero.mpr h21) (vsub_ne_zero.mpr h32) diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean index d32ef29050ef2..16f7d52a36180 100644 --- a/Mathlib/Geometry/Manifold/BumpFunction.lean +++ b/Mathlib/Geometry/Manifold/BumpFunction.lean @@ -34,7 +34,7 @@ variable {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] -open Function Filter FiniteDimensional Set Metric +open Function Filter Module Set Metric open scoped Topology Manifold diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index 6b82e8495e419..f5d59a6f08222 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -67,7 +67,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] noncomputable section -open Metric FiniteDimensional Function +open Metric Module Function open scoped Manifold diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 23d818e090332..07606636dad70 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -57,7 +57,7 @@ smooth bump function, partition of unity universe uι uE uH uM uF -open Function Filter FiniteDimensional Set +open Function Filter Module Set open scoped Topology Manifold noncomputable section diff --git a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean index e99bb7ea3797f..3e3f2e4bb92fd 100644 --- a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean +++ b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean @@ -31,7 +31,7 @@ variable {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] -open Function Filter FiniteDimensional Set +open Function Filter Module Set open scoped Manifold noncomputable section diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index e0cc46543b743..935dc82abfb3b 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -29,14 +29,14 @@ section AffineSpace' variable (k : Type*) {V : Type*} {P : Type*} variable {ι : Type*} -open AffineSubspace FiniteDimensional Module +open AffineSubspace Module variable [DivisionRing k] [AddCommGroup V] [Module k V] [AffineSpace V P] /-- The `vectorSpan` of a finite set is finite-dimensional. -/ theorem finiteDimensional_vectorSpan_of_finite {s : Set P} (h : Set.Finite s) : FiniteDimensional k (vectorSpan k s) := - span_of_finite k <| h.vsub h + .span_of_finite k <| h.vsub h /-- The `vectorSpan` of a family indexed by a `Fintype` is finite-dimensional. -/ @@ -202,7 +202,7 @@ theorem finrank_vectorSpan_le_iff_not_affineIndependent [Fintype ι] (p : ι → variable {k} lemma AffineIndependent.card_le_finrank_succ [Fintype ι] {p : ι → P} (hp : AffineIndependent k p) : - Fintype.card ι ≤ FiniteDimensional.finrank k (vectorSpan k (Set.range p)) + 1 := by + Fintype.card ι ≤ Module.finrank k (vectorSpan k (Set.range p)) + 1 := by cases isEmpty_or_nonempty ι · simp [Fintype.card_eq_zero] rw [← tsub_le_iff_right] @@ -257,7 +257,7 @@ theorem AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_ad (hi : AffineIndependent k p) {s : Finset ι} {sm : Submodule k V} [FiniteDimensional k sm] (hle : vectorSpan k (s.image p : Set P) ≤ sm) (hc : Finset.card s = finrank k sm + 1) : vectorSpan k (s.image p : Set P) = sm := - eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan_image_finset hc + Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan_image_finset hc /-- If the `vectorSpan` of a finite affinely independent family lies in a submodule with dimension one less than its @@ -266,7 +266,7 @@ theorem AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one [Fintyp (hi : AffineIndependent k p) {sm : Submodule k V} [FiniteDimensional k sm] (hle : vectorSpan k (Set.range p) ≤ sm) (hc : Fintype.card ι = finrank k sm + 1) : vectorSpan k (Set.range p) = sm := - eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan hc + Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan hc /-- If the `affineSpan` of a finite subset of an affinely independent family lies in an affine subspace whose direction has dimension one @@ -669,7 +669,7 @@ section DivisionRing variable {k : Type*} {V : Type*} {P : Type*} -open AffineSubspace FiniteDimensional Module +open AffineSubspace Module Module variable [DivisionRing k] [AddCommGroup V] [Module k V] [AffineSpace V P] @@ -764,12 +764,12 @@ protected theorem finite_set [FiniteDimensional k V] {s : Set ι} (b : AffineBas finite_set_of_fin_dim_affineIndependent k b.ind theorem card_eq_finrank_add_one [Fintype ι] (b : AffineBasis ι k P) : - Fintype.card ι = FiniteDimensional.finrank k V + 1 := + Fintype.card ι = Module.finrank k V + 1 := have : FiniteDimensional k V := b.finiteDimensional b.ind.affineSpan_eq_top_iff_card_eq_finrank_add_one.mp b.tot theorem exists_affineBasis_of_finiteDimensional [Fintype ι] [FiniteDimensional k V] - (h : Fintype.card ι = FiniteDimensional.finrank k V + 1) : Nonempty (AffineBasis ι k P) := by + (h : Fintype.card ι = Module.finrank k V + 1) : Nonempty (AffineBasis ι k P) := by obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P lift s to Finset P using b.finite_set refine ⟨b.reindex <| Fintype.equivOfCardEq ?_⟩ diff --git a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean index 169819f4632df..bff969f2c534c 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean @@ -302,7 +302,7 @@ lemma inf_orthogonal_self_le_ker_restrict {W : Submodule R M} (b₁ : B.IsRefl) variable [FiniteDimensional K V] -open FiniteDimensional Submodule +open Module Submodule variable {B : BilinForm K V} diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean index eff887d7c175d..a54a424f7f68e 100644 --- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean +++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean @@ -51,7 +51,7 @@ section Coeff theorem charpoly_monic : f.charpoly.Monic := Matrix.charpoly_monic _ -open FiniteDimensional in +open Module in lemma charpoly_natDegree [Nontrivial R] [StrongRankCondition R] : natDegree (charpoly f) = finrank R M := by rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex] diff --git a/Mathlib/LinearAlgebra/Coevaluation.lean b/Mathlib/LinearAlgebra/Coevaluation.lean index bd0df67099a43..31b64ef5ce5f8 100644 --- a/Mathlib/LinearAlgebra/Coevaluation.lean +++ b/Mathlib/LinearAlgebra/Coevaluation.lean @@ -25,7 +25,7 @@ noncomputable section section coevaluation -open TensorProduct FiniteDimensional +open TensorProduct Module open TensorProduct diff --git a/Mathlib/LinearAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/Contraction.lean index 8ba1276a30496..0e7e5c811a68a 100644 --- a/Mathlib/LinearAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/Contraction.lean @@ -201,7 +201,7 @@ section CommRing variable [CommRing R] variable [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] variable [Module R M] [Module R N] [Module R P] [Module R Q] -variable [Free R M] [Finite R M] [Free R N] [Finite R N] +variable [Free R M] [Module.Finite R M] [Free R N] [Module.Finite R N] /-- When `M` is a finite free module, the map `lTensorHomToHomLTensor` is an equivalence. Note that `lTensorHomEquivHomLTensor` is not defined directly in terms of diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index ce891c2dddd94..8f8edaca16e32 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -231,15 +231,15 @@ theorem det_id : LinearMap.det (LinearMap.id : M →ₗ[A] M) = 1 := @[simp] theorem det_smul {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] (c : 𝕜) (f : M →ₗ[𝕜] M) : - LinearMap.det (c • f) = c ^ FiniteDimensional.finrank 𝕜 M * LinearMap.det f := by + LinearMap.det (c • f) = c ^ Module.finrank 𝕜 M * LinearMap.det f := by by_cases H : ∃ s : Finset M, Nonempty (Basis s 𝕜 M) · have : FiniteDimensional 𝕜 M := by rcases H with ⟨s, ⟨hs⟩⟩ exact FiniteDimensional.of_fintype_basis hs - simp only [← det_toMatrix (FiniteDimensional.finBasis 𝕜 M), LinearEquiv.map_smul, + simp only [← det_toMatrix (Module.finBasis 𝕜 M), LinearEquiv.map_smul, Fintype.card_fin, Matrix.det_smul] · classical - have : FiniteDimensional.finrank 𝕜 M = 0 := finrank_eq_zero_of_not_exists_basis H + have : Module.finrank 𝕜 M = 0 := finrank_eq_zero_of_not_exists_basis H simp [coe_det, H, this] theorem det_zero' {ι : Type*} [Finite ι] [Nonempty ι] (b : Basis ι A M) : @@ -253,7 +253,7 @@ and `0` otherwise. We give a formula that also works in infinite dimension, wher the determinant to be `1`. -/ @[simp] theorem det_zero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] : - LinearMap.det (0 : M →ₗ[𝕜] M) = (0 : 𝕜) ^ FiniteDimensional.finrank 𝕜 M := by + LinearMap.det (0 : M →ₗ[𝕜] M) = (0 : 𝕜) ^ Module.finrank 𝕜 M := by simp only [← zero_smul 𝕜 (1 : M →ₗ[𝕜] M), det_smul, mul_one, MonoidHom.map_one] theorem det_eq_one_of_subsingleton [Subsingleton M] (f : M →ₗ[R] M) : @@ -263,14 +263,14 @@ theorem det_eq_one_of_subsingleton [Subsingleton M] (f : M →ₗ[R] M) : exact Matrix.det_isEmpty theorem det_eq_one_of_finrank_eq_zero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] - [Module 𝕜 M] (h : FiniteDimensional.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) : + [Module 𝕜 M] (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) : LinearMap.det (f : M →ₗ[𝕜] M) = 1 := by classical refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl intro s b have : IsEmpty s := by rw [← Fintype.card_eq_zero_iff] - exact (FiniteDimensional.finrank_eq_card_basis b).symm.trans h + exact (Module.finrank_eq_card_basis b).symm.trans h exact Matrix.det_isEmpty /-- Conjugating a linear map by a linear equiv does not change its determinant. -/ @@ -423,8 +423,8 @@ theorem LinearEquiv.coe_ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' determinant is nonzero. -/ abbrev LinearMap.equivOfDetNeZero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] [FiniteDimensional 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 0) : M ≃ₗ[𝕜] M := - have : IsUnit (LinearMap.toMatrix (FiniteDimensional.finBasis 𝕜 M) - (FiniteDimensional.finBasis 𝕜 M) f).det := by + have : IsUnit (LinearMap.toMatrix (Module.finBasis 𝕜 M) + (Module.finBasis 𝕜 M) f).det := by rw [LinearMap.det_toMatrix] exact isUnit_iff_ne_zero.2 hf LinearEquiv.ofIsUnitDet this diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean index 2a3358623db3a..9a7b997644973 100644 --- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean +++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean @@ -35,7 +35,7 @@ universe u v v' u₁' w w' variable {R S : Type u} {M : Type v} {M' : Type v'} {M₁ : Type v} variable {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*} -open Cardinal Basis Submodule Function Set FiniteDimensional DirectSum +open Basis Cardinal DirectSum Function Module Set Submodule variable [Ring R] [CommRing S] [AddCommGroup M] [AddCommGroup M'] [AddCommGroup M₁] variable [Module R M] @@ -142,7 +142,7 @@ theorem rank_prod' : Module.rank R (M × M₁) = Module.rank R M + Module.rank R /-- The finrank of `M × M'` is `(finrank R M) + (finrank R M')`. -/ @[simp] -theorem FiniteDimensional.finrank_prod [Module.Finite R M] [Module.Finite R M'] : +theorem Module.finrank_prod [Module.Finite R M] [Module.Finite R M'] : finrank R (M × M') = finrank R M + finrank R M' := by simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M'] @@ -209,7 +209,7 @@ theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] : open Fintype -namespace FiniteDimensional +namespace Module @[simp] theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ M) = card ι * finrank R M := by @@ -234,7 +234,7 @@ theorem finrank_directSum {ι : Type v} [Fintype ι] (M : ι → Type w) [∀ i theorem finrank_matrix (m n : Type*) [Fintype m] [Fintype n] : finrank R (Matrix m n R) = card m * card n := by simp [finrank] -end FiniteDimensional +end Module end Finsupp @@ -260,13 +260,13 @@ theorem rank_pi [Finite η] : Module.rank R (∀ i, φ i) = variable (R) /-- The finrank of `(ι → R)` is `Fintype.card ι`. -/ -theorem FiniteDimensional.finrank_pi {ι : Type v} [Fintype ι] : +theorem Module.finrank_pi {ι : Type v} [Fintype ι] : finrank R (ι → R) = Fintype.card ι := by simp [finrank] --TODO: this should follow from `LinearEquiv.finrank_eq`, that is over a field. /-- The finrank of a finite product is the sum of the finranks. -/ -theorem FiniteDimensional.finrank_pi_fintype +theorem Module.finrank_pi_fintype {ι : Type v} [Fintype ι] {M : ι → Type w} [∀ i : ι, AddCommGroup (M i)] [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] : finrank R (∀ i, M i) = ∑ i, finrank R (M i) := by @@ -294,12 +294,12 @@ variable (R) /-- The vector space of functions on a `Fintype ι` has finrank equal to the cardinality of `ι`. -/ @[simp] -theorem FiniteDimensional.finrank_fintype_fun_eq_card : finrank R (η → R) = Fintype.card η := +theorem Module.finrank_fintype_fun_eq_card : finrank R (η → R) = Fintype.card η := finrank_eq_of_rank_eq rank_fun' /-- The vector space of functions on `Fin n` has finrank equal to `n`. -/ -- @[simp] -- Porting note (#10618): simp already proves this -theorem FiniteDimensional.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by simp +theorem Module.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by simp variable {R} @@ -343,7 +343,7 @@ theorem rank_tensorProduct' : /-- The `S`-finrank of `M ⊗[R] M'` is `(finrank S M) * (finrank R M')`. -/ @[simp] -theorem FiniteDimensional.finrank_tensorProduct : +theorem Module.finrank_tensorProduct : finrank R (M ⊗[S] M') = finrank R M * finrank S M' := by simp [finrank] end TensorProduct @@ -352,7 +352,7 @@ section SubmoduleRank section -open FiniteDimensional +open Module namespace Submodule @@ -413,7 +413,7 @@ theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ := (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _) -open Submodule FiniteDimensional +open Submodule Module variable (R) diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index 81356f0bed052..cf1afda61d172 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -12,7 +12,7 @@ import Mathlib.LinearAlgebra.Dimension.RankNullity /-! # Dimension of vector spaces -In this file we provide results about `Module.rank` and `FiniteDimensional.finrank` of vector spaces +In this file we provide results about `Module.rank` and `Module.finrank` of vector spaces over division rings. ## Main statements @@ -112,7 +112,7 @@ end Module section Basis -open FiniteDimensional +open Module variable [DivisionRing K] [AddCommGroup V] [Module K V] diff --git a/Mathlib/LinearAlgebra/Dimension/Finite.lean b/Mathlib/LinearAlgebra/Dimension/Finite.lean index 32cbe00cac733..5e70194888971 100644 --- a/Mathlib/LinearAlgebra/Dimension/Finite.lean +++ b/Mathlib/LinearAlgebra/Dimension/Finite.lean @@ -26,7 +26,7 @@ variable [Module R M] [Module R M'] [Module R M₁] attribute [local instance] nontrivial_of_invariantBasisNumber -open Cardinal Basis Submodule Function Set FiniteDimensional +open Basis Cardinal Function Module Set Submodule theorem rank_le {n : ℕ} (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) : @@ -363,7 +363,7 @@ variable [Nontrivial R] /-- A (finite dimensional) space that is a subsingleton has zero `finrank`. -/ @[nontriviality] -theorem FiniteDimensional.finrank_zero_of_subsingleton [Subsingleton M] : +theorem Module.finrank_zero_of_subsingleton [Subsingleton M] : finrank R M = 0 := by rw [finrank, rank_subsingleton', _root_.map_zero] @@ -374,12 +374,12 @@ section variable [NoZeroSMulDivisors R M] /-- A finite dimensional space is nontrivial if it has positive `finrank`. -/ -theorem FiniteDimensional.nontrivial_of_finrank_pos (h : 0 < finrank R M) : Nontrivial M := +theorem Module.nontrivial_of_finrank_pos (h : 0 < finrank R M) : Nontrivial M := rank_pos_iff_nontrivial.mp (lt_rank_of_lt_finrank h) /-- A finite dimensional space is nontrivial if it has `finrank` equal to the successor of a natural number. -/ -theorem FiniteDimensional.nontrivial_of_finrank_eq_succ {n : ℕ} +theorem Module.nontrivial_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Nontrivial M := nontrivial_of_finrank_pos (R := R) (by rw [hn]; exact n.succ_pos) @@ -398,31 +398,31 @@ section StrongRankCondition variable [StrongRankCondition R] [Module.Finite R M] /-- A finite rank torsion-free module has positive `finrank` iff it has a nonzero element. -/ -theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero [NoZeroSMulDivisors R M] : +theorem Module.finrank_pos_iff_exists_ne_zero [NoZeroSMulDivisors R M] : 0 < finrank R M ↔ ∃ x : M, x ≠ 0 := by rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank] norm_cast /-- An `R`-finite torsion-free module has positive `finrank` iff it is nontrivial. -/ -theorem FiniteDimensional.finrank_pos_iff [NoZeroSMulDivisors R M] : +theorem Module.finrank_pos_iff [NoZeroSMulDivisors R M] : 0 < finrank R M ↔ Nontrivial M := by rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank] norm_cast /-- A nontrivial finite dimensional space has positive `finrank`. -/ -theorem FiniteDimensional.finrank_pos [NoZeroSMulDivisors R M] [h : Nontrivial M] : +theorem Module.finrank_pos [NoZeroSMulDivisors R M] [h : Nontrivial M] : 0 < finrank R M := finrank_pos_iff.mpr h -/-- See `FiniteDimensional.finrank_zero_iff` +/-- See `Module.finrank_zero_iff` for the stronger version with `NoZeroSMulDivisors R M`. -/ -theorem FiniteDimensional.finrank_eq_zero_iff : +theorem Module.finrank_eq_zero_iff : finrank R M = 0 ↔ ∀ x : M, ∃ a : R, a ≠ 0 ∧ a • x = 0 := by rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank] norm_cast /-- The `StrongRankCondition` is automatic. See `commRing_strongRankCondition`. -/ -theorem FiniteDimensional.finrank_eq_zero_iff_isTorsion {R} [CommRing R] [StrongRankCondition R] +theorem Module.finrank_eq_zero_iff_isTorsion {R} [CommRing R] [StrongRankCondition R] [IsDomain R] [Module R M] [Module.Finite R M] : finrank R M = 0 ↔ Module.IsTorsion R M := by rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank] @@ -430,14 +430,14 @@ theorem FiniteDimensional.finrank_eq_zero_iff_isTorsion {R} [CommRing R] [Strong /-- A finite dimensional space has zero `finrank` iff it is a subsingleton. This is the `finrank` version of `rank_zero_iff`. -/ -theorem FiniteDimensional.finrank_zero_iff [NoZeroSMulDivisors R M] : +theorem Module.finrank_zero_iff [NoZeroSMulDivisors R M] : finrank R M = 0 ↔ Subsingleton M := by rw [← rank_zero_iff (R := R), ← finrank_eq_rank] norm_cast end StrongRankCondition -theorem FiniteDimensional.finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) : +theorem Module.finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) : finrank R M = 0 := by delta finrank rw [h, zero_toNat] diff --git a/Mathlib/LinearAlgebra/Dimension/Finrank.lean b/Mathlib/LinearAlgebra/Dimension/Finrank.lean index 9bf3954c81775..69668ef8b667a 100644 --- a/Mathlib/LinearAlgebra/Dimension/Finrank.lean +++ b/Mathlib/LinearAlgebra/Dimension/Finrank.lean @@ -13,7 +13,7 @@ Definition of the rank of a module, or dimension of a vector space, as a natural ## Main definitions -Defined is `FiniteDimensional.finrank`, the dimension of a finite dimensional space, returning a +Defined is `Module.finrank`, the dimension of a finite dimensional space, returning a `Nat`, as opposed to `Module.rank`, which returns a `Cardinal`. When the space has infinite dimension, its `finrank` is by convention set to `0`. @@ -38,7 +38,7 @@ open Cardinal Submodule Module Function variable {R : Type u} {M : Type v} {N : Type w} variable [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] -namespace FiniteDimensional +namespace Module section Ring @@ -52,6 +52,8 @@ of `M` over `R`. noncomputable def finrank (R M : Type*) [Semiring R] [AddCommGroup M] [Module R M] : ℕ := Cardinal.toNat (Module.rank R M) +@[deprecated (since := "2024-10-01")] protected alias _root_.FiniteDimensional.finrank := finrank + theorem finrank_eq_of_rank_eq {n : ℕ} (h : Module.rank R M = ↑n) : finrank R M = n := by apply_fun toNat at h rw [toNat_natCast] at h @@ -92,9 +94,9 @@ theorem finrank_le_finrank_of_rank_le_rank end Ring -end FiniteDimensional +end Module -open FiniteDimensional +open Module namespace LinearEquiv diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean index 3b06f6f965e75..af3007b4da717 100644 --- a/Mathlib/LinearAlgebra/Dimension/Free.lean +++ b/Mathlib/LinearAlgebra/Dimension/Free.lean @@ -14,7 +14,7 @@ import Mathlib.SetTheory.Cardinal.Finsupp ## Main result - `LinearEquiv.nonempty_equiv_iff_lift_rank_eq`: Two free modules are isomorphic iff they have the same dimension. -- `FiniteDimensional.finBasis`: +- `Module.finBasis`: An arbitrary basis of a finite free module indexed by `Fin n` given `finrank R M = n`. -/ @@ -24,7 +24,7 @@ noncomputable section universe u v v' w -open Cardinal Basis Submodule Function Set DirectSum FiniteDimensional +open Cardinal Basis Submodule Function Set DirectSum Module section Tower @@ -57,7 +57,7 @@ theorem rank_mul_rank (A : Type v) [AddCommGroup A] /-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/ -theorem FiniteDimensional.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := by +theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := by simp_rw [finrank] rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul, lift_rank_mul_lift_rank, toNat_lift] @@ -79,7 +79,7 @@ theorem rank_eq_card_chooseBasisIndex : Module.rank R M = #(ChooseBasisIndex R M (chooseBasis R M).mk_eq_rank''.symm /-- The finrank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/ -theorem _root_.FiniteDimensional.finrank_eq_card_chooseBasisIndex [Module.Finite R M] : +theorem _root_.Module.finrank_eq_card_chooseBasisIndex [Module.Finite R M] : finrank R M = Fintype.card (ChooseBasisIndex R M) := by simp [finrank, rank_eq_card_chooseBasisIndex] @@ -161,35 +161,30 @@ noncomputable def LinearEquiv.ofFinrankEq [Module.Finite R M] [Module.Finite R M variable {M M'} +namespace Module + /-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/ -lemma Module.rank_lt_alpeh0_iff : - Module.rank R M < ℵ₀ ↔ Module.Finite R M := by +lemma rank_lt_aleph0_iff : Module.rank R M < ℵ₀ ↔ Module.Finite R M := by rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff] exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M), fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩ -theorem FiniteDimensional.finrank_of_not_finite - (h : ¬Module.Finite R M) : - finrank R M = 0 := by - rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_alpeh0_iff] +theorem finrank_of_not_finite (h : ¬Module.Finite R M) : finrank R M = 0 := by + rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff] exact .inr h -theorem Module.finite_of_finrank_pos (h : 0 < finrank R M) : - Module.Finite R M := by +theorem finite_of_finrank_pos (h : 0 < finrank R M) : Module.Finite R M := by contrapose h simp [finrank_of_not_finite h] -theorem Module.finite_of_finrank_eq_succ {n : ℕ} - (hn : finrank R M = n.succ) : Module.Finite R M := - Module.finite_of_finrank_pos <| by rw [hn]; exact n.succ_pos +theorem finite_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Module.Finite R M := + finite_of_finrank_pos <| by rw [hn]; exact n.succ_pos -theorem Module.finite_iff_of_rank_eq_nsmul {W} [AddCommGroup W] - [Module R W] [Module.Free R W] {n : ℕ} (hn : n ≠ 0) - (hVW : Module.rank R M = n • Module.rank R W) : +theorem finite_iff_of_rank_eq_nsmul {W} [AddCommGroup W] [Module R W] [Module.Free R W] {n : ℕ} + (hn : n ≠ 0) (hVW : Module.rank R M = n • Module.rank R W) : Module.Finite R M ↔ Module.Finite R W := by - simp only [← rank_lt_alpeh0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn] + simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn] -namespace FiniteDimensional variable (R M) /-- A finite rank free module has a basis indexed by `Fin (finrank R M)`. -/ @@ -220,4 +215,4 @@ theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι] (basisUnique ι h).repr.map_eq_zero_iff.mp (Finsupp.ext fun j => Subsingleton.elim i j ▸ hv), fun hv => by rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]⟩ -end FiniteDimensional +end Module diff --git a/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean index 507f9e3b737de..17254b66084e3 100644 --- a/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean +++ b/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean @@ -17,7 +17,7 @@ and `Mathlib/LinearAlgebra/FiniteDimensional.lean`. -/ -open Cardinal Submodule Set FiniteDimensional +open Cardinal Module Module Set Submodule universe u v @@ -27,7 +27,7 @@ variable {K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGrou /-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional. -See also `FiniteDimensional.finBasis`. +See also `Module.finBasis`. -/ noncomputable def Basis.ofRankEqZero [Module.Free K V] {ι : Type*} [IsEmpty ι] (hV : Module.rank K V = 0) : Basis ι K V := @@ -186,7 +186,7 @@ theorem finrank_eq_one_iff [Module.Free K V] (ι : Type*) [Unique ι] : finrank K V = 1 ↔ Nonempty (Basis ι K V) := by constructor · intro h - exact ⟨basisUnique ι h⟩ + exact ⟨Module.basisUnique ι h⟩ · rintro ⟨b⟩ simpa using finrank_eq_card_basis b diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean index 215eca3c7a657..b6445fadfe529 100644 --- a/Mathlib/LinearAlgebra/Dimension/Localization.lean +++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean @@ -15,9 +15,9 @@ import Mathlib.RingTheory.OreLocalization.OreSet - `IsLocalizedModule.lift_rank_eq`: `rank_Rₚ Mₚ = rank R M`. - `rank_quotient_add_rank_of_isDomain`: The **rank-nullity theorem** for commutative domains. - -/ -open Cardinal nonZeroDivisors + +open Cardinal Module nonZeroDivisors section CommRing diff --git a/Mathlib/LinearAlgebra/Dimension/RankNullity.lean b/Mathlib/LinearAlgebra/Dimension/RankNullity.lean index 1e94b3ea6e179..2e6cb6ba25096 100644 --- a/Mathlib/LinearAlgebra/Dimension/RankNullity.lean +++ b/Mathlib/LinearAlgebra/Dimension/RankNullity.lean @@ -171,7 +171,7 @@ theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule R M) : section Finrank -open Submodule FiniteDimensional +open Submodule Module variable [StrongRankCondition R] diff --git a/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean index aecd0ad209da8..12001f79238c5 100644 --- a/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean +++ b/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean @@ -376,14 +376,12 @@ theorem Ideal.rank_eq {R S : Type*} [CommRing R] [StrongRankCondition R] [Ring S ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective))) (c.card_le_card_of_linearIndependent this) -open FiniteDimensional +namespace Module theorem finrank_eq_nat_card_basis (h : Basis ι R M) : finrank R M = Nat.card ι := by rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank] -namespace FiniteDimensional - /-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis. -/ theorem finrank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) : @@ -392,8 +390,8 @@ theorem finrank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) : /-- If a free module is of finite rank, then the cardinality of any basis is equal to its `finrank`. -/ -theorem _root_.Module.mk_finrank_eq_card_basis [Module.Finite R M] - {ι : Type w} (h : Basis ι R M) : (finrank R M : Cardinal.{w}) = #ι := by +theorem mk_finrank_eq_card_basis [Module.Finite R M] {ι : Type w} (h : Basis ι R M) : + (finrank R M : Cardinal.{w}) = #ι := by cases @nonempty_fintype _ (Module.Finite.finite_basis h) rw [Cardinal.mk_fintype, finrank_eq_card_basis h] @@ -402,10 +400,6 @@ cardinality of the basis. This lemma uses a `Finset` instead of indexed types. - theorem finrank_eq_card_finset_basis {ι : Type w} {b : Finset ι} (h : Basis b R M) : finrank R M = Finset.card b := by rw [finrank_eq_card_basis h, Fintype.card_coe] -end FiniteDimensional - -open FiniteDimensional - variable (R) @[simp] @@ -415,15 +409,15 @@ theorem rank_self : Module.rank R R = 1 := by /-- A ring satisfying `StrongRankCondition` (such as a `DivisionRing`) is one-dimensional as a module over itself. -/ @[simp] -theorem FiniteDimensional.finrank_self : finrank R R = 1 := +theorem finrank_self : finrank R R = 1 := finrank_eq_of_rank_eq (by simp) /-- Given a basis of a ring over itself indexed by a type `ι`, then `ι` is `Unique`. -/ -noncomputable def Basis.unique {ι : Type*} (b : Basis ι R R) : Unique ι := by - have A : Cardinal.mk ι = ↑(FiniteDimensional.finrank R R) := +noncomputable def _root_.Basis.unique {ι : Type*} (b : Basis ι R R) : Unique ι := by + have A : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm -- Porting note: replace `algebraMap.coe_one` with `Nat.cast_one` - simp only [Cardinal.eq_one_iff_unique, FiniteDimensional.finrank_self, Nat.cast_one] at A + simp only [Cardinal.eq_one_iff_unique, Module.finrank_self, Nat.cast_one] at A exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 A) variable (M) @@ -436,19 +430,15 @@ theorem rank_lt_aleph0 [Module.Finite R M] : Module.rank R M < ℵ₀ := by refine (ciSup_le' fun i => ?_).trans_lt (nat_lt_aleph0 S.card) exact linearIndependent_le_span_finset _ i.prop S hS -@[deprecated (since := "2024-01-01")] -protected alias FiniteDimensional.rank_lt_aleph0 := rank_lt_aleph0 - /-- If `M` is finite, `finrank M = rank M`. -/ @[simp] -theorem finrank_eq_rank [Module.Finite R M] : - ↑(FiniteDimensional.finrank R M) = Module.rank R M := by - rw [FiniteDimensional.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)] +theorem finrank_eq_rank [Module.Finite R M] : ↑(finrank R M) = Module.rank R M := by + rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)] + +end Module -@[deprecated (since := "2024-01-01")] -protected alias FiniteDimensional.finrank_eq_rank := finrank_eq_rank +open Module -variable {R M} variable {M'} [AddCommGroup M'] [Module R M'] theorem LinearMap.finrank_le_finrank_of_injective [Module.Finite R M'] {f : M →ₗ[R] M'} diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index b4d2e69e8d184..1d2a2669cab75 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -91,6 +91,8 @@ The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to splitting of `V₁`. -/ +open Module Submodule + noncomputable section namespace Module @@ -384,7 +386,7 @@ theorem toDualEquiv_apply (m : M) : b.toDualEquiv m = b.toDual m := theorem linearEquiv_dual_iff_finiteDimensional [Field K] [AddCommGroup V] [Module K V] : Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V := by refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩ - rw [FiniteDimensional, ← Module.rank_lt_alpeh0_iff] + rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff] by_contra! apply (lift_rank_lt_rank_dual this).ne have := e.lift_rank_eq @@ -449,12 +451,12 @@ theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) : section -variable [Finite R M] [Free R M] +variable [Module.Finite R M] [Free R M] instance dual_free : Free R (Dual R M) := Free.of_basis (Free.chooseBasis R M).dualBasis -instance dual_finite : Finite R (Dual R M) := +instance dual_finite : Module.Finite R (Dual R M) := Finite.of_basis (Free.chooseBasis R M).dualBasis end @@ -482,7 +484,7 @@ universe uK uV variable {K : Type uK} {V : Type uV} variable [CommRing K] [AddCommGroup V] [Module K V] [Module.Free K V] -open Module Module.Dual Submodule LinearMap Cardinal Basis FiniteDimensional +open Module Module.Dual Submodule LinearMap Cardinal Basis Module section @@ -540,7 +542,7 @@ theorem nontrivial_dual_iff : instance instNontrivialDual [Nontrivial V] : Nontrivial (Dual K V) := (nontrivial_dual_iff K).mpr inferInstance -theorem finite_dual_iff : Finite K (Dual K V) ↔ Finite K V := by +theorem finite_dual_iff : Module.Finite K (Dual K V) ↔ Module.Finite K V := by constructor <;> intro h · obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V) nontriviality K @@ -578,7 +580,7 @@ class IsReflexive : Prop where lemma bijective_dual_eval [IsReflexive R M] : Bijective (Dual.eval R M) := IsReflexive.bijective_dual_eval' -instance IsReflexive.of_finite_of_free [Finite R M] [Free R M] : IsReflexive R M where +instance IsReflexive.of_finite_of_free [Module.Finite R M] [Free R M] : IsReflexive R M where bijective_dual_eval' := ⟨LinearMap.ker_eq_bot.mp (Free.chooseBasis R M).eval_ker, LinearMap.range_eq_top.mp (Free.chooseBasis R M).eval_range⟩ @@ -1057,7 +1059,7 @@ theorem dualEquivDual_apply (φ : Module.Dual K W) : section -open FiniteDimensional +open FiniteDimensional Module instance instModuleDualFiniteDimensional [FiniteDimensional K V] : FiniteDimensional K (Module.Dual K V) := by @@ -1096,7 +1098,7 @@ noncomputable def quotEquivAnnihilator (W : Subspace K V) : (V ⧸ W) ≃ₗ[K] -- refine' LinearEquiv.quot_equiv_of_equiv _ (Basis.ofVectorSpace K V).toDualEquiv -- exact (Basis.ofVectorSpace K W).toDualEquiv.trans W.dual_equiv_dual -open FiniteDimensional +open Module @[simp] theorem finrank_dualCoannihilator_eq {Φ : Subspace K (Module.Dual K V)} : @@ -1231,7 +1233,7 @@ theorem dualQuotEquivDualAnnihilator_symm_apply_mk (W : Submodule R M) (φ : W.d rfl theorem finite_dualAnnihilator_iff {W : Submodule R M} [Free R (M ⧸ W)] : - Finite R W.dualAnnihilator ↔ Finite R (M ⧸ W) := + Module.Finite R W.dualAnnihilator ↔ Module.Finite R (M ⧸ W) := (Finite.equiv_iff W.dualQuotEquivDualAnnihilator.symm).trans (finite_dual_iff R) open LinearMap in @@ -1324,7 +1326,6 @@ lemma range_eq_top_of_ne_zero : rw [eq_top_iff] exact fun x _ ↦ ⟨x • (f v)⁻¹ • v, by simp [inv_mul_cancel₀ hv]⟩ -open FiniteDimensional variable [FiniteDimensional K V₁] lemma finrank_ker_add_one_of_ne_zero : @@ -1479,7 +1480,7 @@ end Subspace section FiniteDimensional -open FiniteDimensional LinearMap +open Module LinearMap namespace LinearMap @@ -1610,7 +1611,7 @@ theorem dualAnnihilator_dualAnnihilator_eq_map (W : Subspace K V) [FiniteDimensi haveI := e1.finiteDimensional let e2 := (Free.chooseBasis K _).toDualEquiv ≪≫ₗ W.dualAnnihilator.dualQuotEquivDualAnnihilator haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2 - rw [FiniteDimensional.eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)] + rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)] rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq] exact e2.finrank_eq diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index 1495ca7c3ce48..3effed50341ef 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -53,7 +53,7 @@ namespace Module namespace End -open FiniteDimensional Set +open Module Set variable {K R : Type v} {V M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Field K] [AddCommGroup V] [Module K V] diff --git a/Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean b/Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean index 561d462974d51..e6cf66f99d9ea 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean @@ -21,7 +21,7 @@ namespace Module namespace End -open Polynomial FiniteDimensional +open Polynomial Module open scoped Polynomial diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index a6fb4ee72e490..c0f53eccf53f8 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -38,7 +38,7 @@ generalized eigenspaces span the whole space. eigenspace, eigenvector, eigenvalue, eigen -/ -open Set Function Module FiniteDimensional +open Set Function Module Module variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] diff --git a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean index f2439bd876a5f..30837353e1b0a 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean @@ -33,7 +33,7 @@ variable {R K M : Type*} [CommRing R] [IsDomain R] [Field K] [AddCommGroup M] variable [Module R M] [Module.Finite R M] [Module.Free R M] variable [Module K M] [Module.Finite K M] -open FiniteDimensional Module.Free Polynomial +open Module Module.Free Polynomial lemma IsNilpotent.charpoly_eq_X_pow_finrank (φ : Module.End R M) (h : IsNilpotent φ) : φ.charpoly = X ^ finrank R M := by diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean index 8aec07c6ff9dd..7b2f68f6cdcdd 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean @@ -27,7 +27,7 @@ variable {K : Type u} {V : Type v} namespace Submodule -open IsNoetherian FiniteDimensional +open IsNoetherian Module section DivisionRing @@ -116,7 +116,7 @@ end FiniteDimensional namespace LinearMap -open FiniteDimensional +open Module section DivisionRing @@ -142,7 +142,7 @@ end DivisionRing end LinearMap -open FiniteDimensional +open Module namespace LinearMap diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean index 7802cfc81de05..acd30d6e430a9 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean @@ -27,7 +27,7 @@ that all these points of view are equivalent, with the following lemmas - `fintypeBasisIndex` states that a finite-dimensional vector space has a finite basis -- `FiniteDimensional.finBasis` and `FiniteDimensional.finBasisOfFinrankEq` +- `Module.finBasis` and `Module.finBasisOfFinrankEq` are bases for finite dimensional vector spaces, where the index type is `Fin` (in `Mathlib.LinearAlgebra.Dimension.Free`) - `of_fintype_basis` states that the existence of a basis indexed by a @@ -70,7 +70,7 @@ Plenty of the results hold for general fg modules or notherian modules, and they universe u v v' w -open Cardinal Submodule Module Function +open Cardinal Function IsNoetherian Module Submodule /-- `FiniteDimensional` vector spaces are defined to be finite modules. Use `FiniteDimensional.of_fintype_basis` to prove finite dimension from another definition. -/ @@ -80,11 +80,6 @@ abbrev FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module variable {K : Type u} {V : Type v} namespace FiniteDimensional - -open IsNoetherian - -section DivisionRing - variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] @@ -145,10 +140,8 @@ theorem of_finite_basis {ι : Type w} {s : Set ι} (h : Basis s K V) (hs : Set.F instance finiteDimensional_submodule [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K S := by letI : IsNoetherian K V := iff_fg.2 ?_ - · exact - iff_fg.1 - (IsNoetherian.iff_rank_lt_aleph0.2 - ((Submodule.rank_le _).trans_lt (_root_.rank_lt_aleph0 K V))) + · exact iff_fg.1 <| IsNoetherian.iff_rank_lt_aleph0.2 <| + (Submodule.rank_le _).trans_lt (rank_lt_aleph0 K V) · infer_instance /-- A quotient of a finite-dimensional space is also finite-dimensional. -/ @@ -156,18 +149,6 @@ instance finiteDimensional_quotient [FiniteDimensional K V] (S : Submodule K V) FiniteDimensional K (V ⧸ S) := Module.Finite.quotient K S -variable (K V) - -/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its -`finrank`. This is a copy of `finrank_eq_rank _ _` which creates easier typeclass searches. -/ -theorem finrank_eq_rank' [FiniteDimensional K V] : (finrank K V : Cardinal.{v}) = Module.rank K V := - finrank_eq_rank _ _ - -variable {K V} - -theorem finrank_of_infinite_dimensional (h : ¬FiniteDimensional K V) : finrank K V = 0 := - FiniteDimensional.finrank_of_not_finite h - theorem of_finrank_pos (h : 0 < finrank K V) : FiniteDimensional K V := Module.finite_of_finrank_pos h @@ -181,6 +162,24 @@ theorem of_fact_finrank_eq_succ (n : ℕ) [hn : Fact (finrank K V = n + 1)] : FiniteDimensional K V := of_finrank_eq_succ hn.out +end FiniteDimensional + +namespace Module + +variable (K V) +variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] + [Module K V₂] + +/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its +`finrank`. This is a copy of `finrank_eq_rank _ _` which creates easier typeclass searches. -/ +theorem finrank_eq_rank' [FiniteDimensional K V] : (finrank K V : Cardinal.{v}) = Module.rank K V := + finrank_eq_rank _ _ + +variable {K V} + +theorem finrank_of_infinite_dimensional (h : ¬FiniteDimensional K V) : finrank K V = 0 := + Module.finrank_of_not_finite h + theorem finiteDimensional_iff_of_rank_eq_nsmul {W} [AddCommGroup W] [Module K W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank K V = n • Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W := @@ -192,6 +191,13 @@ theorem finrank_eq_card_basis' [FiniteDimensional K V] {ι : Type w} (h : Basis (finrank K V : Cardinal.{w}) = #ι := Module.mk_finrank_eq_card_basis h +end Module + +namespace FiniteDimensional +section DivisionRing +variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] + [Module K V₂] + theorem _root_.LinearIndependent.lt_aleph0_of_finiteDimensional {ι : Type w} [FiniteDimensional K V] {v : ι → V} (h : LinearIndependent K v) : #ι < ℵ₀ := h.lt_aleph0_of_finite @@ -254,8 +260,6 @@ section open Finset -section - variable {L : Type*} [LinearOrderedField L] variable {W : Type v} [AddCommGroup W] [Module L W] @@ -271,16 +275,14 @@ theorem exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card [Finite exact ⟨f, sum, total, exists_pos_of_sum_zero_of_exists_nonzero f total nonzero⟩ -end - end /-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/ @[simps repr_apply] noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) : Basis ι K V := - let b := FiniteDimensional.basisUnique ι h - let h : b.repr v default ≠ 0 := mt FiniteDimensional.basisUnique_repr_eq_zero_iff.mp hv + let b := Module.basisUnique ι h + let h : b.repr v default ≠ 0 := mt Module.basisUnique_repr_eq_zero_iff.mp hv Basis.ofRepr { toFun := fun w => Finsupp.single default (b.repr w default / b.repr v default) invFun := fun f => f default • v @@ -326,8 +328,6 @@ section ZeroRank variable [DivisionRing K] [AddCommGroup V] [Module K V] -open FiniteDimensional - theorem FiniteDimensional.of_rank_eq_nat {n : ℕ} (h : Module.rank K V = n) : FiniteDimensional K V := Module.finite_of_rank_eq_nat h @@ -350,7 +350,7 @@ alias finiteDimensional_of_rank_eq_one := FiniteDimensional.of_rank_eq_one variable (K V) instance finiteDimensional_bot : FiniteDimensional K (⊥ : Submodule K V) := - of_rank_eq_zero <| by simp + .of_rank_eq_zero <| by simp variable {K V} @@ -358,7 +358,7 @@ end ZeroRank namespace Submodule -open IsNoetherian FiniteDimensional +open IsNoetherian Module section DivisionRing @@ -423,7 +423,7 @@ end Submodule namespace LinearEquiv -open FiniteDimensional +open Module variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] @@ -448,10 +448,7 @@ instance finiteDimensional_finsupp {ι : Type*} [Finite ι] [FiniteDimensional K end -namespace FiniteDimensional - -section DivisionRing - +namespace Submodule variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] @@ -469,33 +466,29 @@ theorem eq_of_le_of_finrank_eq {S₁ S₂ : Submodule K V} [FiniteDimensional K (hd : finrank K S₁ = finrank K S₂) : S₁ = S₂ := eq_of_le_of_finrank_le hle hd.ge -section Subalgebra +end Submodule + +namespace Subalgebra variable {K L : Type*} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L} [hfin : FiniteDimensional K E] /-- If a subalgebra is contained in a finite-dimensional subalgebra with the same or smaller dimension, they are equal. -/ -theorem _root_.Subalgebra.eq_of_le_of_finrank_le (h_le : F ≤ E) - (h_finrank : finrank K E ≤ finrank K F) : F = E := +theorem eq_of_le_of_finrank_le (h_le : F ≤ E) (h_finrank : finrank K E ≤ finrank K F) : F = E := haveI : Module.Finite K (Subalgebra.toSubmodule E) := hfin - Subalgebra.toSubmodule_injective <| FiniteDimensional.eq_of_le_of_finrank_le h_le h_finrank + toSubmodule_injective <| Submodule.eq_of_le_of_finrank_le h_le h_finrank /-- If a subalgebra is contained in a finite-dimensional subalgebra with the same dimension, they are equal. -/ -theorem _root_.Subalgebra.eq_of_le_of_finrank_eq (h_le : F ≤ E) - (h_finrank : finrank K F = finrank K E) : F = E := - Subalgebra.eq_of_le_of_finrank_le h_le h_finrank.ge +theorem eq_of_le_of_finrank_eq (h_le : F ≤ E) (h_finrank : finrank K F = finrank K E) : F = E := + eq_of_le_of_finrank_le h_le h_finrank.ge end Subalgebra -end DivisionRing - -end FiniteDimensional - namespace LinearMap -open FiniteDimensional +open Module section DivisionRing @@ -599,7 +592,7 @@ end LinearMap namespace LinearEquiv -open FiniteDimensional +open Module variable [DivisionRing K] [AddCommGroup V] [Module K V] variable [FiniteDimensional K V] @@ -646,14 +639,14 @@ theorem isUnit_iff_range_eq_top [FiniteDimensional K V] (f : V →ₗ[K] V) : end LinearMap -open Module FiniteDimensional +open FiniteDimensional Module section variable [DivisionRing K] [AddCommGroup V] [Module K V] theorem finrank_zero_iff_forall_zero [FiniteDimensional K V] : finrank K V = 0 ↔ ∀ x : V, x = 0 := - FiniteDimensional.finrank_zero_iff.trans (subsingleton_iff_forall_eq 0) + Module.finrank_zero_iff.trans (subsingleton_iff_forall_eq 0) /-- If `ι` is an empty type and `V` is zero-dimensional, there is a unique `ι`-indexed basis. -/ noncomputable def basisOfFinrankZero [FiniteDimensional K V] {ι : Type*} [IsEmpty ι] diff --git a/Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean b/Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean index d0b35b5f4be62..27e40eb067043 100644 --- a/Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean +++ b/Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean @@ -26,7 +26,7 @@ variable (R : Type u) (S : Type u') (M : Type v) (N : Type w) open Module.Free (chooseBasis ChooseBasisIndex) -open FiniteDimensional (finrank) +open Module (finrank) section Ring @@ -46,27 +46,27 @@ instance Module.Finite.linearMap [Module.Finite S N] : Module.Finite S (M →ₗ variable [StrongRankCondition R] [StrongRankCondition S] [Module.Free S N] open Cardinal -theorem FiniteDimensional.rank_linearMap : +theorem Module.rank_linearMap : Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N) := by rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul, ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast] /-- The finrank of `M →ₗ[R] N` as an `S`-module is `(finrank R M) * (finrank S N)`. -/ -theorem FiniteDimensional.finrank_linearMap : +theorem Module.finrank_linearMap : finrank S (M →ₗ[R] N) = finrank R M * finrank S N := by simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift] variable [Module R S] [SMulCommClass R S S] -theorem FiniteDimensional.rank_linearMap_self : +theorem Module.rank_linearMap_self : Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M) := by rw [rank_linearMap, rank_self, lift_one, mul_one] -theorem FiniteDimensional.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M := by +theorem Module.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M := by rw [finrank_linearMap, finrank_self, mul_one] @[deprecated (since := "2024-01-12")] -alias FiniteDimensional.finrank_linear_map' := FiniteDimensional.finrank_linearMap_self +alias Module.finrank_linear_map' := Module.finrank_linearMap_self end Ring @@ -84,12 +84,12 @@ theorem cardinal_mk_algHom_le_rank : #(M →ₐ[K] L) ≤ lift.{v} (Module.rank convert (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank · rw [lift_id] · have := Module.nontrivial K L - rw [lift_id, FiniteDimensional.rank_linearMap_self] + rw [lift_id, Module.rank_linearMap_self] theorem card_algHom_le_finrank : Nat.card (M →ₐ[K] L) ≤ finrank K M := by convert toNat_le_toNat (cardinal_mk_algHom_le_rank K M L) ?_ · rw [toNat_lift, finrank] - · rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply rank_lt_aleph0 + · rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply Module.rank_lt_aleph0 end AlgHom diff --git a/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean b/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean index 44870709f726a..054d145f3347d 100644 --- a/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean +++ b/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean @@ -114,9 +114,9 @@ noncomputable def quotientEquivDirectSum : theorem finrank_quotient_eq_sum {ι} [Fintype ι] (b : Basis ι R S) [Nontrivial F] [∀ i, Module.Free F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))] [∀ i, Module.Finite F (R ⧸ span ({I.smithCoeffs b hI i} : Set R))] : - FiniteDimensional.finrank F (S ⧸ I) = - ∑ i, FiniteDimensional.finrank F (R ⧸ span ({I.smithCoeffs b hI i} : Set R)) := by + Module.finrank F (S ⧸ I) = + ∑ i, Module.finrank F (R ⧸ span ({I.smithCoeffs b hI i} : Set R)) := by -- slow, and dot notation doesn't work - rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, FiniteDimensional.finrank_directSum] + rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, Module.finrank_directSum] end Ideal diff --git a/Mathlib/LinearAlgebra/FreeModule/Norm.lean b/Mathlib/LinearAlgebra/FreeModule/Norm.lean index 39bb414d9ce5c..5332fcc328e26 100644 --- a/Mathlib/LinearAlgebra/FreeModule/Norm.lean +++ b/Mathlib/LinearAlgebra/FreeModule/Norm.lean @@ -71,7 +71,7 @@ instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) : `F`-vector space is the degree of the norm of `f` relative to `F[X]`. -/ theorem finrank_quotient_span_eq_natDegree_norm [Algebra F S] [IsScalarTower F F[X] S] (b : Basis ι F[X] S) {f : S} (hf : f ≠ 0) : - FiniteDimensional.finrank F (S ⧸ span ({f} : Set S)) = (Algebra.norm F[X] f).natDegree := by + Module.finrank F (S ⧸ span ({f} : Set S)) = (Algebra.norm F[X] f).natDegree := by haveI := Fintype.ofFinite ι have h := span_singleton_eq_bot.not.2 hf rw [natDegree_eq_of_degree_eq diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean index 8d2b791e900da..d7867798bc310 100644 --- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean +++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean @@ -27,7 +27,7 @@ variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] variable [Fintype K] [Finite V] local notation "q" => Fintype.card K -local notation "n" => FiniteDimensional.finrank K V +local notation "n" => Module.finrank K V attribute [local instance] Fintype.ofFinite in open Fintype in @@ -86,8 +86,8 @@ theorem card_GL_field : rcases Nat.eq_zero_or_pos n with rfl | hn · simp [Nat.card_eq_fintype_card] · rw [Nat.card_congr (equiv_GL_linearindependent n hn), card_linearIndependent, - FiniteDimensional.finrank_fintype_fun_eq_card, Fintype.card_fin] - simp only [FiniteDimensional.finrank_fintype_fun_eq_card, Fintype.card_fin, le_refl] + Module.finrank_fintype_fun_eq_card, Fintype.card_fin] + simp only [Module.finrank_fintype_fun_eq_card, Fintype.card_fin, le_refl] end field diff --git a/Mathlib/LinearAlgebra/Orientation.lean b/Mathlib/LinearAlgebra/Orientation.lean index 68891b346f5df..549ff52629c7b 100644 --- a/Mathlib/LinearAlgebra/Orientation.lean +++ b/Mathlib/LinearAlgebra/Orientation.lean @@ -326,7 +326,7 @@ namespace Orientation variable [Fintype ι] -open FiniteDimensional +open FiniteDimensional Module /-- If the index type has cardinality equal to the finite dimension, any two orientations are equal or negations. -/ diff --git a/Mathlib/LinearAlgebra/Projectivization/Basic.lean b/Mathlib/LinearAlgebra/Projectivization/Basic.lean index fd5d3d6aa6db7..94d4e7925bb43 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Basic.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Basic.lean @@ -78,7 +78,7 @@ theorem rep_nonzero (v : ℙ K V) : v.rep ≠ 0 := @[simp] theorem mk_rep (v : ℙ K V) : mk K v.rep v.rep_nonzero = v := Quotient.out_eq' _ -open FiniteDimensional +open Module /-- Consider an element of the projectivization as a submodule of `V`. -/ protected def submodule (v : ℙ K V) : Submodule K V := diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 7eba713353773..fe2fe2b66dfe2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -1180,7 +1180,7 @@ theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticForm_ne_zero hB₁ exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩ -open FiniteDimensional +open Module variable {V : Type u} {K : Type v} [Field K] [AddCommGroup V] [Module K V] variable [FiniteDimensional K V] @@ -1194,7 +1194,7 @@ theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinFo haveI := finrank_pos_iff.1 (hd.symm ▸ Nat.succ_pos d : 0 < finrank K V) -- either the bilinear form is trivial or we can pick a non-null `x` obtain rfl | hB₁ := eq_or_ne B 0 - · let b := FiniteDimensional.finBasis K V + · let b := Module.finBasis K V rw [hd] at b exact ⟨b, fun i j _ => rfl⟩ obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean index 3285feacba1f0..8f1a7a9b3e50d 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean @@ -70,7 +70,7 @@ noncomputable def isometryEquivSumSquaresUnits (w : ι → Units ℂ) : the sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`. -/ theorem equivalent_sum_squares {M : Type*} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M] (Q : QuadraticForm ℂ M) (hQ : (associated (R := ℂ) Q).SeparatingLeft) : - Equivalent Q (weightedSumSquares ℂ (1 : Fin (FiniteDimensional.finrank ℂ M) → ℂ)) := + Equivalent Q (weightedSumSquares ℂ (1 : Fin (Module.finrank ℂ M) → ℂ)) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ ⟨hw₁.trans (isometryEquivSumSquaresUnits w)⟩ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean index ff5c68946f2d8..567af287573fc 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean @@ -141,7 +141,7 @@ variable [Field K] [Invertible (2 : K)] [AddCommGroup V] [Module K V] /-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of squares. -/ noncomputable def isometryEquivWeightedSumSquares (Q : QuadraticForm K V) - (v : Basis (Fin (FiniteDimensional.finrank K V)) K V) + (v : Basis (Fin (Module.finrank K V)) K V) (hv₁ : (associated (R := K) Q).IsOrthoᵢ v) : Q.IsometryEquiv (weightedSumSquares K fun i => Q (v i)) := by let iso := Q.isometryEquivBasisRepr v @@ -154,13 +154,13 @@ variable [FiniteDimensional K V] open LinearMap.BilinForm theorem equivalent_weightedSumSquares (Q : QuadraticForm K V) : - ∃ w : Fin (FiniteDimensional.finrank K V) → K, Equivalent Q (weightedSumSquares K w) := + ∃ w : Fin (Module.finrank K V) → K, Equivalent Q (weightedSumSquares K w) := let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm _ Q) ⟨_, ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩ theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm K V) (hQ : (associated (R := K) Q).SeparatingLeft) : - ∃ w : Fin (FiniteDimensional.finrank K V) → Kˣ, Equivalent Q (weightedSumSquares K w) := by + ∃ w : Fin (Module.finrank K V) → Kˣ, Equivalent Q (weightedSumSquares K w) := by obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q) have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ simp_rw [LinearMap.IsOrtho, associated_eq_self_apply] at hv₂ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean index 7ec3a6f4947d8..b9fe9bdf90ae3 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Real.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Real.lean @@ -53,7 +53,7 @@ noncomputable def isometryEquivSignWeightedSumSquares (w : ι → ℝ) : sum of squares with the weights being ±1, `SignType` version. -/ theorem equivalent_sign_ne_zero_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) : - ∃ w : Fin (FiniteDimensional.finrank ℝ M) → SignType, + ∃ w : Fin (Module.finrank ℝ M) → SignType, (∀ i, w i ≠ 0) ∧ Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ ⟨sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_ne_zero.2 (w i).ne_zero, @@ -63,7 +63,7 @@ theorem equivalent_sign_ne_zero_weighted_sum_squared {M : Type*} [AddCommGroup M sum of squares with the weights being ±1. -/ theorem equivalent_one_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) : - ∃ w : Fin (FiniteDimensional.finrank ℝ M) → ℝ, + ∃ w : Fin (Module.finrank ℝ M) → ℝ, (∀ i, w i = -1 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) := let ⟨w, hw₀, hw⟩ := Q.equivalent_sign_ne_zero_weighted_sum_squared hQ ⟨(w ·), fun i ↦ by cases hi : w i <;> simp_all, hw⟩ @@ -72,7 +72,7 @@ theorem equivalent_one_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] sum of squares with the weights being ±1 or 0, `SignType` version. -/ theorem equivalent_signType_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) : - ∃ w : Fin (FiniteDimensional.finrank ℝ M) → SignType, + ∃ w : Fin (Module.finrank ℝ M) → SignType, Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) := let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares ⟨sign ∘ w, ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩ @@ -81,7 +81,7 @@ theorem equivalent_signType_weighted_sum_squared {M : Type*} [AddCommGroup M] [M sum of squares with the weights being ±1 or 0. -/ theorem equivalent_one_zero_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) : - ∃ w : Fin (FiniteDimensional.finrank ℝ M) → ℝ, + ∃ w : Fin (Module.finrank ℝ M) → ℝ, (∀ i, w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) := let ⟨w, hw⟩ := Q.equivalent_signType_weighted_sum_squared ⟨(w ·), fun i ↦ by cases h : w i <;> simp [h], hw⟩ diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean index ea02d0bd4374e..0b3d984857b62 100644 --- a/Mathlib/LinearAlgebra/Semisimple.lean +++ b/Mathlib/LinearAlgebra/Semisimple.lean @@ -145,7 +145,7 @@ theorem IsSemisimple.minpoly_squarefree : Squarefree (minpoly K f) := protected theorem IsSemisimple.aeval (p : K[X]) : (aeval f p).IsSemisimple := let R := K[X] ⧸ Ideal.span {minpoly K f} - have : Finite K R := + have : Module.Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| Algebra.IsIntegral.isIntegral f).finite have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <| span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical @@ -174,9 +174,9 @@ theorem IsSemisimple.of_mem_adjoin_pair {a : End K M} (ha : a ∈ Algebra.adjoin a.IsSemisimple := by let R := K[X] ⧸ Ideal.span {minpoly K f} let S := AdjoinRoot ((minpoly K g).map <| algebraMap K R) - have : Finite K R := + have : Module.Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| Algebra.IsIntegral.isIntegral f).finite - have : Finite R S := + have : Module.Finite R S := (AdjoinRoot.powerBasis' <| (minpoly.monic <| Algebra.IsIntegral.isIntegral g).map _).finite #adaptation_note /-- @@ -187,7 +187,7 @@ theorem IsSemisimple.of_mem_adjoin_pair {a : End K M} (ha : a ∈ Algebra.adjoin -/ set_option maxSynthPendingDepth 2 in have : IsScalarTower K R S := .of_algebraMap_eq fun _ ↦ rfl - have : Finite K S := .trans R S + have : Module.Finite K S := .trans R S have : IsArtinianRing R := .of_finite K R have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <| span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical diff --git a/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean b/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean index 2ec0b351ea9e9..83b52e58279fd 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean @@ -36,7 +36,7 @@ mainly used in the definition of linearly disjointness. open scoped TensorProduct -open FiniteDimensional +open Module noncomputable section @@ -194,7 +194,7 @@ theorem rank_sup_le_of_free [Module.Free R A] [Module.Free R B] : exact rank_range_le (A.mulMap B).toLinearMap /-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are -free `R`-algebras, then the `FiniteDimensional.finrank` of `A ⊔ B` is less than or equal to +free `R`-algebras, then the `Module.finrank` of `A ⊔ B` is less than or equal to the product of that of `A` and `B`. -/ theorem finrank_sup_le_of_free [Module.Free R A] [Module.Free R B] : finrank R ↥(A ⊔ B) ≤ finrank R A * finrank R B := by @@ -206,7 +206,7 @@ theorem finrank_sup_le_of_free [Module.Free R A] [Module.Free R B] : wlog hA : ¬ Module.Finite R A generalizing A B · have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA)) rwa [sup_comm, mul_comm] at this - rw [← Module.rank_lt_alpeh0_iff, not_lt] at hA + rw [← Module.rank_lt_aleph0_iff, not_lt] at hA have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <| show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA, diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean index d8dfa8fb4f30b..81598681a3b50 100644 --- a/Mathlib/LinearAlgebra/Trace.lean +++ b/Mathlib/LinearAlgebra/Trace.lean @@ -25,7 +25,7 @@ universe u v w namespace LinearMap open scoped Matrix -open FiniteDimensional TensorProduct +open Module TensorProduct section diff --git a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean index 76566b1a9cc1e..2b64a512ceb6e 100644 --- a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean +++ b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean @@ -27,7 +27,7 @@ for a general nontrivial normed space. open Set Function Metric MeasurableSpace intervalIntegral open scoped Pointwise ENNReal NNReal -local notation "dim" => FiniteDimensional.finrank ℝ +local notation "dim" => Module.finrank ℝ noncomputable section namespace MeasureTheory @@ -39,7 +39,7 @@ namespace Measure /-- If `μ` is an additive Haar measure on a normed space `E`, then `μ.toSphere` is the measure on the unit sphere in `E` -such that `μ.toSphere s = FiniteDimensional.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s)`. -/ +such that `μ.toSphere s = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s)`. -/ def toSphere (μ : Measure E) : Measure (sphere (0 : E) 1) := dim E • ((μ.comap (Subtype.val ∘ (homeomorphUnitSphereProd E).symm)).restrict (univ ×ˢ Iio ⟨1, mem_Ioi.2 one_pos⟩)).fst @@ -106,7 +106,7 @@ instance (n : ℕ) : SigmaFinite (volumeIoiPow n) := /-- The homeomorphism `homeomorphUnitSphereProd E` sends an additive Haar measure `μ` to the product of `μ.toSphere` and `MeasureTheory.Measure.volumeIoiPow (dim E - 1)`, -where `dim E = FiniteDimensional.finrank ℝ E` is the dimension of `E`. -/ +where `dim E = Module.finrank ℝ E` is the dimension of `E`. -/ theorem measurePreserving_homeomorphUnitSphereProd : MeasurePreserving (homeomorphUnitSphereProd E) (μ.comap (↑)) (μ.toSphere.prod (volumeIoiPow (dim E - 1))) := by @@ -119,7 +119,7 @@ theorem measurePreserving_homeomorphUnitSphereProd : fun s hs ↦ forall_mem_range.2 fun r ↦ ?_ have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by rw [LinearOrderedField.smul_Ioo r.2.out, smul_zero, smul_eq_mul, mul_one] - have hpos : 0 < dim E := FiniteDimensional.finrank_pos + have hpos : 0 < dim E := Module.finrank_pos rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio, comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this, smul_assoc, μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos, diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean index 60ca4af5a4851..2c3bc40927bd3 100644 --- a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean +++ b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean @@ -43,7 +43,7 @@ In particular, this number is bounded by `5 ^ dim` by a straightforward measure universe u -open Metric Set FiniteDimensional MeasureTheory Filter Fin +open Metric Set Module MeasureTheory Filter Fin open scoped ENNReal Topology diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index 3b9bc2e1d765d..ce6116b747cb5 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -87,7 +87,7 @@ Change of variables in integrals [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2] -/ -open MeasureTheory MeasureTheory.Measure Metric Filter Set FiniteDimensional Asymptotics +open MeasureTheory MeasureTheory.Measure Metric Filter Set Module Asymptotics TopologicalSpace open scoped NNReal ENNReal Topology Pointwise @@ -1185,7 +1185,7 @@ theorem det_one_smulRight {𝕜 : Type*} [NormedField 𝕜] (v : 𝕜) : Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply, mul_one] rw [this, ContinuousLinearMap.det, ContinuousLinearMap.coe_smul, ContinuousLinearMap.one_def, ContinuousLinearMap.coe_id, LinearMap.det_smul, - FiniteDimensional.finrank_self, LinearMap.det_id, pow_one, mul_one] + Module.finrank_self, LinearMap.det_id, pow_one, mul_one] /-- Integrability in the change of variable formula for differentiable functions (one-variable version): if a function `f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then a diff --git a/Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean b/Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean index df01cd8cae6c3..4f7644744e85c 100644 --- a/Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean +++ b/Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean @@ -36,7 +36,7 @@ Hermann Minkowski. namespace MeasureTheory -open ENNReal FiniteDimensional MeasureTheory MeasureTheory.Measure Set Filter +open ENNReal Module MeasureTheory MeasureTheory.Measure Set Filter open scoped Pointwise NNReal diff --git a/Mathlib/MeasureTheory/Integral/PeakFunction.lean b/Mathlib/MeasureTheory/Integral/PeakFunction.lean index df652367ebf11..845644d23d8fb 100644 --- a/Mathlib/MeasureTheory/Integral/PeakFunction.lean +++ b/Mathlib/MeasureTheory/Integral/PeakFunction.lean @@ -392,7 +392,7 @@ theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuou ### Peak functions of the form `x ↦ c ^ dim * φ (c x)` -/ -open FiniteDimensional Bornology +open Module Bornology variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {μ : Measure F} [IsAddHaarMeasure μ] diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index cc3daa531971b..71eec8c794d88 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean @@ -16,7 +16,7 @@ measure `1` to the parallelepiped spanned by any orthonormal basis, and that it the canonical `volume` from the `MeasureSpace` instance. -/ -open FiniteDimensional MeasureTheory MeasureTheory.Measure Set +open Module MeasureTheory MeasureTheory.Measure Set variable {ι E F : Type*} diff --git a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean index 29af339ad2552..a4030ed00f9d7 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean @@ -18,7 +18,7 @@ open scoped NNReal ENNReal Pointwise Topology open Inv Set Function MeasureTheory.Measure Filter -open FiniteDimensional +open Module namespace MeasureTheory @@ -122,11 +122,11 @@ alias set_integral_comp_smul_of_pos := setIntegral_comp_smul_of_pos theorem integral_comp_mul_left (g : ℝ → F) (a : ℝ) : (∫ x : ℝ, g (a * x)) = |a⁻¹| • ∫ y : ℝ, g y := by - simp_rw [← smul_eq_mul, Measure.integral_comp_smul, FiniteDimensional.finrank_self, pow_one] + simp_rw [← smul_eq_mul, Measure.integral_comp_smul, Module.finrank_self, pow_one] theorem integral_comp_inv_mul_left (g : ℝ → F) (a : ℝ) : (∫ x : ℝ, g (a⁻¹ * x)) = |a| • ∫ y : ℝ, g y := by - simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, FiniteDimensional.finrank_self, pow_one] + simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one] theorem integral_comp_mul_right (g : ℝ → F) (a : ℝ) : (∫ x : ℝ, g (x * a)) = |a⁻¹| • ∫ y : ℝ, g y := by diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean index 18ebba51fd6f0..8bbb057670b05 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean @@ -26,7 +26,7 @@ of the basis). -/ -open Set TopologicalSpace MeasureTheory MeasureTheory.Measure FiniteDimensional +open Set TopologicalSpace MeasureTheory MeasureTheory.Measure Module open scoped Pointwise diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index e03f24092e1a1..497ba69408ba9 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -109,7 +109,7 @@ Hausdorff measure, measure, metric measure open scoped NNReal ENNReal Topology -open EMetric Set Function Filter Encodable FiniteDimensional TopologicalSpace +open EMetric Set Function Filter Encodable Module TopologicalSpace noncomputable section diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index 54c09f7095a7a..9ede8fdf04384 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -100,7 +100,7 @@ theorem Basis.map_addHaar {ι E F : Type*} [Fintype ι] [NormedAddCommGroup E] [ namespace MeasureTheory -open Measure TopologicalSpace.PositiveCompacts FiniteDimensional +open Measure TopologicalSpace.PositiveCompacts Module /-! ### The Lebesgue measure is a Haar measure on `ℝ` and on `ℝ^ι`. diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean index 110086e7b6708..73abc051da088 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean @@ -40,7 +40,7 @@ Using these formulas, we compute the volume of the unit balls in several cases. section general_case -open MeasureTheory MeasureTheory.Measure FiniteDimensional ENNReal +open MeasureTheory MeasureTheory.Measure Module ENNReal theorem MeasureTheory.measure_unitBall_eq_integral_div_gamma {E : Type*} {p : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] @@ -160,7 +160,7 @@ end general_case section LpSpace -open Real Fintype ENNReal FiniteDimensional MeasureTheory MeasureTheory.Measure +open Real Fintype ENNReal Module MeasureTheory MeasureTheory.Measure variable (ι : Type*) [Fintype ι] {p : ℝ} @@ -350,7 +350,7 @@ end EuclideanSpace section InnerProductSpace -open MeasureTheory MeasureTheory.Measure ENNReal Real FiniteDimensional +open MeasureTheory MeasureTheory.Measure ENNReal Real Module variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 20d24352136cb..3c95d15cc13ee 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -58,7 +58,7 @@ included in the `Cyclotomic` locale. -/ -open Polynomial Algebra FiniteDimensional Set +open Polynomial Algebra Module Set universe u v w z diff --git a/Mathlib/NumberTheory/Cyclotomic/Embeddings.lean b/Mathlib/NumberTheory/Cyclotomic/Embeddings.lean index b3d2a56cf11a2..642d6933fad59 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Embeddings.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Embeddings.lean @@ -21,7 +21,7 @@ universe u namespace IsCyclotomicExtension.Rat -open NumberField InfinitePlace FiniteDimensional Complex Nat Polynomial +open NumberField InfinitePlace Module Complex Nat Polynomial variable {n : ℕ+} (K : Type u) [Field K] [CharZero K] diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 33bb6cad832cd..a9c07d9408500 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -61,7 +61,7 @@ and only at the "final step", when we need to provide an "explicit" primitive ro -/ -open Polynomial Algebra Finset FiniteDimensional IsCyclotomicExtension Nat PNat Set +open Polynomial Algebra Finset Module IsCyclotomicExtension Nat PNat Set open scoped IntermediateField universe u v w z @@ -182,7 +182,7 @@ least `(lcm p q).totient`. -/ theorem _root_.IsPrimitiveRoot.lcm_totient_le_finrank [FiniteDimensional K L] {p q : ℕ} {x y : L} (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) (hirr : Irreducible (cyclotomic (Nat.lcm p q) K)) : - (Nat.lcm p q).totient ≤ FiniteDimensional.finrank K L := by + (Nat.lcm p q).totient ≤ Module.finrank K L := by rcases Nat.eq_zero_or_pos p with (rfl | hppos) · simp rcases Nat.eq_zero_or_pos q with (rfl | hqpos) @@ -439,7 +439,7 @@ theorem norm_pow_sub_one_of_prime_pow_ne_two {k s : ℕ} (hζ : IsPrimitiveRoot congr · rw [PNat.pow_coe, Nat.pow_minFac, hpri.1.minFac_eq] exact Nat.succ_ne_zero _ - have := FiniteDimensional.finrank_mul_finrank K K⟮η⟯ L + have := Module.finrank_mul_finrank K K⟮η⟯ L rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁, PNat.pow_coe, PNat.pow_coe, Nat.totient_prime_pow hpri.out (k - s).succ_pos, Nat.totient_prime_pow hpri.out k.succ_pos, mul_comm _ ((p : ℕ) - 1), mul_assoc, diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index 2093382c27cb9..425189bfa3c7b 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -69,9 +69,9 @@ theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt] refine IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;> simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply] constructor <;> intro h - · let b := FiniteDimensional.finBasis (RatFunc Fq) F + · let b := Module.finBasis (RatFunc Fq) F exact FiniteDimensional.of_fintype_basis (b.mapCoeffs e this) - · let b := FiniteDimensional.finBasis Fqt F + · let b := Module.finBasis Fqt F refine FiniteDimensional.of_fintype_basis (b.mapCoeffs e.symm ?_) intro c x; convert (this (e.symm c) x).symm; simp only [e.apply_symm_apply] diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean index 7aef3e02c40b2..cd142c881c370 100644 --- a/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/Basic.lean @@ -307,7 +307,7 @@ theorem mem_span_integralBasis {x : K} : rw [integralBasis, Basis.localizationLocalization_span, LinearMap.mem_range, IsScalarTower.coe_toAlgHom', RingHom.mem_range] -theorem RingOfIntegers.rank : FiniteDimensional.finrank ℤ (𝓞 K) = FiniteDimensional.finrank ℚ K := +theorem RingOfIntegers.rank : Module.finrank ℤ (𝓞 K) = Module.finrank ℚ K := IsIntegralClosure.rank ℤ ℚ K (𝓞 K) end NumberField diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean index 5970d297810cb..c62e465bc30d5 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean @@ -100,7 +100,7 @@ theorem integerLattice.inter_ball_finite [NumberField K] (r : ℝ) : · rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩ exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩ -open Module Fintype FiniteDimensional +open Module Fintype Module /-- A `ℂ`-basis of `ℂ^n` that is also a `ℤ`-basis of the `integerLattice`. -/ noncomputable def latticeBasis [NumberField K] : @@ -176,7 +176,7 @@ end NumberField.canonicalEmbedding namespace NumberField.mixedEmbedding -open NumberField.InfinitePlace FiniteDimensional Finset +open NumberField.InfinitePlace Module Finset /-- The mixed space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/ abbrev mixedSpace := @@ -491,7 +491,7 @@ def indexEquiv : (index K) ≃ (K →+* ℂ) := by · exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩, by simp [(embedding_mk_eq φ).resolve_left hw]⟩ · rw [Embeddings.card, ← mixedEmbedding.finrank K, - ← FiniteDimensional.finrank_eq_card_basis (stdBasis K)] + ← Module.finrank_eq_card_basis (stdBasis K)] variable {K} diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index eb0293caf7695..36a06aabe738b 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -40,7 +40,7 @@ variable (K : Type*) [Field K] namespace NumberField.mixedEmbedding -open NumberField NumberField.InfinitePlace FiniteDimensional +open NumberField NumberField.InfinitePlace Module section convexBodyLT @@ -450,7 +450,7 @@ end convexBodySum section minkowski open scoped Classical -open MeasureTheory MeasureTheory.Measure FiniteDimensional ZSpan Real Submodule +open MeasureTheory MeasureTheory.Measure Module ZSpan Real Submodule open scoped ENNReal NNReal nonZeroDivisors IntermediateField diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean index 223002432594b..419b0f6e623c0 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean @@ -87,7 +87,7 @@ end UnitSMul noncomputable section logMap -open NumberField.Units NumberField.Units.dirichletUnitTheorem FiniteDimensional +open NumberField.Units NumberField.Units.dirichletUnitTheorem Module variable [NumberField K] {K} diff --git a/Mathlib/NumberTheory/NumberField/ClassNumber.lean b/Mathlib/NumberTheory/NumberField/ClassNumber.lean index 992a53910d440..06ed53e2b5316 100644 --- a/Mathlib/NumberTheory/NumberField/ClassNumber.lean +++ b/Mathlib/NumberTheory/NumberField/ClassNumber.lean @@ -41,7 +41,7 @@ variable {K} theorem classNumber_eq_one_iff : classNumber K = 1 ↔ IsPrincipalIdealRing (𝓞 K) := card_classGroup_eq_one_iff -open FiniteDimensional NumberField.InfinitePlace +open Module NumberField.InfinitePlace open scoped nonZeroDivisors Real diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean index 85e0a1770c687..b56a1d4722194 100644 --- a/Mathlib/NumberTheory/NumberField/Discriminant.lean +++ b/Mathlib/NumberTheory/NumberField/Discriminant.lean @@ -32,7 +32,7 @@ number field, discriminant namespace NumberField -open FiniteDimensional NumberField NumberField.InfinitePlace Matrix +open Module NumberField NumberField.InfinitePlace Matrix open scoped Classical Real nonZeroDivisors diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 40c427c9d06f8..c30dda51f0a43 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -38,7 +38,7 @@ namespace NumberField.Embeddings section Fintype -open FiniteDimensional +open Module variable (K : Type*) [Field K] [NumberField K] variable (A : Type*) [Field A] [CharZero A] @@ -55,7 +55,7 @@ theorem card : Fintype.card (K →+* A) = finrank ℚ K := by instance : Nonempty (K →+* A) := by rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A] - exact FiniteDimensional.finrank_pos + exact Module.finrank_pos end Fintype @@ -78,7 +78,7 @@ end Roots section Bounded -open FiniteDimensional Polynomial Set +open Module Polynomial Set variable {K : Type*} [Field K] [NumberField K] variable {A : Type*} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] @@ -450,7 +450,7 @@ noncomputable instance NumberField.InfinitePlace.fintype [NumberField K] : Fintype (InfinitePlace K) := Set.fintypeRange _ theorem sum_mult_eq [NumberField K] : - ∑ w : InfinitePlace K, mult w = FiniteDimensional.finrank ℚ K := by + ∑ w : InfinitePlace K, mult w = Module.finrank ℚ K := by rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise (fun φ => InfinitePlace.mk φ)] exact Finset.sum_congr rfl @@ -546,7 +546,7 @@ theorem _root_.NumberField.adjoin_eq_top_of_infinitePlace_lt {x : 𝓞 K} {w : I end NumberField -open Fintype FiniteDimensional +open Fintype Module variable (K) @@ -1024,12 +1024,12 @@ lemma IsUnramifiedAtInfinitePlaces_of_odd_card_aut [IsGalois k K] [FiniteDimensi ⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_card_aut_of_not_isUnramified)⟩ lemma IsUnramifiedAtInfinitePlaces_of_odd_finrank [IsGalois k K] - (h : Odd (FiniteDimensional.finrank k K)) : IsUnramifiedAtInfinitePlaces k K := + (h : Odd (Module.finrank k K)) : IsUnramifiedAtInfinitePlaces k K := ⟨fun _ ↦ not_not.mp (Nat.not_even_iff_odd.2 h ∘ InfinitePlace.even_finrank_of_not_isUnramified)⟩ variable (k K) -open FiniteDimensional in +open Module in lemma IsUnramifiedAtInfinitePlaces.card_infinitePlace [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] : Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K := by diff --git a/Mathlib/NumberTheory/NumberField/EquivReindex.lean b/Mathlib/NumberTheory/NumberField/EquivReindex.lean index 67fc4926a8307..0226ce9f8e5d5 100644 --- a/Mathlib/NumberTheory/NumberField/EquivReindex.lean +++ b/Mathlib/NumberTheory/NumberField/EquivReindex.lean @@ -21,7 +21,7 @@ namespace NumberField noncomputable section -open Module.Free FiniteDimensional canonicalEmbedding Matrix Finset +open Module.Free Module canonicalEmbedding Matrix Finset /-- An equivalence between the set of embeddings of `K` into `ℂ` and the index set of the chosen basis of the ring of integers of `K`. -/ diff --git a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean index 47f93f496cc3b..1444de4b7e903 100644 --- a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean +++ b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean @@ -89,7 +89,7 @@ theorem mem_span_basisOfFractionalIdeal {I : (FractionalIdeal (𝓞 K)⁰ K)ˣ} rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _] simp -open FiniteDimensional in +open Module in theorem fractionalIdeal_rank (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : finrank ℤ I = finrank ℤ (𝓞 K) := by rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, diff --git a/Mathlib/NumberTheory/NumberField/House.lean b/Mathlib/NumberTheory/NumberField/House.lean index 5d0cc0062fc60..d56eb4d18c668 100644 --- a/Mathlib/NumberTheory/NumberField/House.lean +++ b/Mathlib/NumberTheory/NumberField/House.lean @@ -27,7 +27,7 @@ namespace NumberField noncomputable section -open Module.Free FiniteDimensional canonicalEmbedding Matrix Finset +open Module.Free Module canonicalEmbedding Matrix Finset attribute [local instance] Matrix.seminormedAddCommGroup @@ -62,7 +62,7 @@ noncomputable section variable (K) -open Module.Free FiniteDimensional canonicalEmbedding Matrix Finset +open Module.Free Module canonicalEmbedding Matrix Finset attribute [local instance] Matrix.seminormedAddCommGroup diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean index 2b529a1d239bb..e8964a687a66b 100644 --- a/Mathlib/NumberTheory/NumberField/Norm.lean +++ b/Mathlib/NumberTheory/NumberField/Norm.lean @@ -22,7 +22,7 @@ rings of integers. open scoped NumberField -open Finset NumberField Algebra FiniteDimensional +open Finset NumberField Algebra Module section Rat diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index 636189cd1f51f..699d1221574f7 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -354,7 +354,7 @@ section statements variable [NumberField K] open scoped Classical -open dirichletUnitTheorem FiniteDimensional +open dirichletUnitTheorem Module /-- The unit rank of the number field `K`, it is equal to `card (InfinitePlace K) - 1`. -/ def rank : ℕ := Fintype.card (InfinitePlace K) - 1 @@ -462,13 +462,13 @@ instance : Monoid.FG (𝓞 K)ˣ := by infer_instance theorem rank_modTorsion : - FiniteDimensional.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by + Module.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by rw [← LinearEquiv.finrank_eq (logEmbeddingEquiv K).symm, unitLattice_rank] /-- A basis of the quotient `(𝓞 K)ˣ ⧸ (torsion K)` seen as an additive ℤ-module. -/ def basisModTorsion : Basis (Fin (rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) := Basis.reindex (Module.Free.chooseBasis ℤ _) (Fintype.equivOfCardEq <| by - rw [← FiniteDimensional.finrank_eq_card_chooseBasisIndex, rank_modTorsion, Fintype.card_fin]) + rw [← Module.finrank_eq_card_chooseBasisIndex, rank_modTorsion, Fintype.card_fin]) /-- The basis of the `unitLattice` obtained by mapping `basisModTorsion` via `logEmbedding`. -/ def basisUnitLattice : Basis (Fin (rank K)) ℤ (unitLattice K) := diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean index c059ce200afdd..c84ce456063d4 100644 --- a/Mathlib/NumberTheory/RamificationInertia.lean +++ b/Mathlib/NumberTheory/RamificationInertia.lean @@ -47,7 +47,7 @@ variable {R : Type u} [CommRing R] variable {S : Type v} [CommRing S] (f : R →+* S) variable (p : Ideal R) (P : Ideal S) -open FiniteDimensional +open Module open UniqueFactorizationMonoid @@ -699,7 +699,7 @@ instance Factors.finiteDimensional_quotient [IsNoetherian R S] [p.IsMaximal] theorem Factors.inertiaDeg_ne_zero [IsNoetherian R S] [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) : inertiaDeg (algebraMap R S) p P ≠ 0 := by - rw [inertiaDeg_algebraMap]; exact (FiniteDimensional.finrank_pos_iff.mpr inferInstance).ne' + rw [inertiaDeg_algebraMap]; exact (Module.finrank_pos_iff.mpr inferInstance).ne' instance Factors.finiteDimensional_quotient_pow [IsNoetherian R S] [p.IsMaximal] (P : (factors (map (algebraMap R S) p)).toFinset) : diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean index e40c61bfaf1ea..b629a2dc92e8b 100644 --- a/Mathlib/RepresentationTheory/Character.lean +++ b/Mathlib/RepresentationTheory/Character.lean @@ -32,7 +32,7 @@ noncomputable section universe u -open CategoryTheory LinearMap CategoryTheory.MonoidalCategory Representation FiniteDimensional +open CategoryTheory LinearMap CategoryTheory.MonoidalCategory Representation Module variable {k : Type u} [Field k] @@ -51,7 +51,7 @@ theorem char_mul_comm (V : FDRep k G) (g : G) (h : G) : V.character (h * g) = V.character (g * h) := by simp only [trace_mul_comm, character, map_mul] @[simp] -theorem char_one (V : FDRep k G) : V.character 1 = FiniteDimensional.finrank k V := by +theorem char_one (V : FDRep k G) : V.character 1 = Module.finrank k V := by simp only [character, map_one, trace_one] /-- The character is multiplicative under the tensor product. -/ diff --git a/Mathlib/RepresentationTheory/FDRep.lean b/Mathlib/RepresentationTheory/FDRep.lean index b19b49f0e400b..1f3f8535f0114 100644 --- a/Mathlib/RepresentationTheory/FDRep.lean +++ b/Mathlib/RepresentationTheory/FDRep.lean @@ -114,7 +114,7 @@ example : MonoidalPreadditive (FDRep k G) := by infer_instance example : MonoidalLinear k (FDRep k G) := by infer_instance -open FiniteDimensional +open Module open scoped Classical diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index f8aba734476d2..86796148fbcf3 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -198,13 +198,13 @@ theorem IsIntegralClosure.module_free [NoZeroSMulDivisors A L] [IsPrincipalIdeal and `L` has no zero smul divisors by `A`, the `A`-rank of the integral closure `C` of `A` in `L` is equal to the `K`-rank of `L`. -/ theorem IsIntegralClosure.rank [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L] : - FiniteDimensional.finrank A C = FiniteDimensional.finrank K L := by + Module.finrank A C = Module.finrank K L := by haveI : Module.Free A C := IsIntegralClosure.module_free A K L C haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := IsIntegralClosure.isLocalization A K L C let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C) - rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex, FiniteDimensional.finrank_eq_card_basis b] + rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b] variable {A K} diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean index b3171e5b848cd..5957f090f0b89 100644 --- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean +++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean @@ -29,7 +29,7 @@ variable (R : Type*) [CommRing R] (K : Type*) [Field K] [Algebra R K] [IsFractio open scoped Multiplicative -open LocalRing FiniteDimensional +open LocalRing Module theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [LocalRing R] [IsDomain R] (h' : (maximalIdeal R).IsPrincipal) (I : Ideal R) (hI : I ≠ ⊥) : diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index f6285f4b7aa27..f3faffa03b668 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -50,7 +50,7 @@ universe u v w z open scoped Matrix -open Matrix FiniteDimensional Fintype Polynomial Finset IntermediateField +open Matrix Module Fintype Polynomial Finset IntermediateField namespace Algebra @@ -190,7 +190,7 @@ theorem discr_powerBasis_eq_prod'' [Algebra.IsSeparable K L] (e : Fin pb.dim ≃ have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp have hle : 1 ≤ pb.dim := by - rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, FiniteDimensional.finrank_pos_iff] + rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, Module.finrank_pos_iff] infer_instance rw [hn, Nat.cast_div h₂ hne, Nat.cast_mul, Nat.cast_sub hle] field_simp diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean index b0366a10493a5..349a1ceec0456 100644 --- a/Mathlib/RingTheory/FiniteType.lean +++ b/Mathlib/RingTheory/FiniteType.lean @@ -45,7 +45,7 @@ section Algebra -- see Note [lower instance priority] instance (priority := 100) finiteType {R : Type*} (A : Type*) [CommSemiring R] [Semiring A] - [Algebra R A] [hRA : Finite R A] : Algebra.FiniteType R A := + [Algebra R A] [hRA : Module.Finite R A] : Algebra.FiniteType R A := ⟨Subalgebra.fg_of_submodule_fg hRA.1⟩ end Algebra @@ -746,7 +746,7 @@ This is similar to `IsNoetherian.injective_of_surjective_endomorphism` but only commutative case, but does not use a Noetherian hypothesis. -/ @[deprecated OrzechProperty.injective_of_surjective_endomorphism (since := "2024-05-30")] theorem Module.Finite.injective_of_surjective_endomorphism {R : Type*} [CommRing R] {M : Type*} - [AddCommGroup M] [Module R M] [Finite R M] (f : M →ₗ[R] M) + [AddCommGroup M] [Module R M] [Module.Finite R M] (f : M →ₗ[R] M) (f_surj : Function.Surjective f) : Function.Injective f := OrzechProperty.injective_of_surjective_endomorphism f f_surj diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index b9e7cb2a2c070..5d61d585d9c03 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -501,7 +501,7 @@ section ModuleAndAlgebra variable (R A B M N : Type*) /-- A module over a semiring is `Finite` if it is finitely generated as a module. -/ -class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where +protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where out : (⊤ : Submodule R M).FG attribute [inherit_doc Module.Finite] Module.Finite.out @@ -511,7 +511,7 @@ namespace Module variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] theorem finite_def {R M} [Semiring R] [AddCommMonoid M] [Module R M] : - Finite R M ↔ (⊤ : Submodule R M).FG := + Module.Finite R M ↔ (⊤ : Submodule R M).FG := ⟨fun h => h.1, fun h => ⟨h⟩⟩ namespace Finite @@ -529,46 +529,47 @@ theorem iff_addGroup_fg {G : Type*} [AddCommGroup G] : Module.Finite ℤ G ↔ A variable {R M N} /-- See also `Module.Finite.exists_fin'`. -/ -theorem exists_fin [Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (range s) = ⊤ := +lemma exists_fin [Module.Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (range s) = ⊤ := Submodule.fg_iff_exists_fin_generating_family.mp out variable (R M) in -lemma exists_fin' [Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f := by +lemma exists_fin' [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f := by have ⟨n, s, hs⟩ := exists_fin (R := R) (M := M) refine ⟨n, Basis.constr (Pi.basisFun R _) ℕ s, ?_⟩ rw [← LinearMap.range_eq_top, Basis.constr_range, hs] -theorem of_surjective [hM : Finite R M] (f : M →ₗ[R] N) (hf : Surjective f) : Finite R N := +theorem of_surjective [hM : Module.Finite R M] (f : M →ₗ[R] N) (hf : Surjective f) : + Module.Finite R N := ⟨by rw [← LinearMap.range_eq_top.2 hf, ← Submodule.map_top] exact hM.1.map f⟩ instance quotient (R) {A M} [Semiring R] [AddCommGroup M] [Ring A] [Module A M] [Module R M] - [SMul R A] [IsScalarTower R A M] [Finite R M] - (N : Submodule A M) : Finite R (M ⧸ N) := + [SMul R A] [IsScalarTower R A M] [Module.Finite R M] + (N : Submodule A M) : Module.Finite R (M ⧸ N) := Module.Finite.of_surjective (N.mkQ.restrictScalars R) N.mkQ_surjective /-- The range of a linear map from a finite module is finite. -/ -instance range {F : Type*} [FunLike F M N] [SemilinearMapClass F (RingHom.id R) M N] [Finite R M] - (f : F) : Finite R (LinearMap.range f) := +instance range {F : Type*} [FunLike F M N] [SemilinearMapClass F (RingHom.id R) M N] + [Module.Finite R M] (f : F) : Module.Finite R (LinearMap.range f) := of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩ /-- Pushforwards of finite submodules are finite. -/ -instance map (p : Submodule R M) [Finite R p] (f : M →ₗ[R] N) : Finite R (p.map f) := +instance map (p : Submodule R M) [Module.Finite R p] (f : M →ₗ[R] N) : Module.Finite R (p.map f) := of_surjective (f.restrict fun _ => Submodule.mem_map_of_mem) fun ⟨_, _, hy, hy'⟩ => ⟨⟨_, hy⟩, Subtype.ext hy'⟩ variable (R) -instance self : Finite R R := +instance self : Module.Finite R R := ⟨⟨{1}, by simpa only [Finset.coe_singleton] using Ideal.span_singleton_one⟩⟩ variable (M) theorem of_restrictScalars_finite (R A M : Type*) [CommSemiring R] [Semiring A] [AddCommMonoid M] - [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] [hM : Finite R M] : - Finite A M := by + [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] [hM : Module.Finite R M] : + Module.Finite A M := by rw [finite_def, Submodule.fg_def] at hM ⊢ obtain ⟨S, hSfin, hSgen⟩ := hM refine ⟨S, hSfin, eq_top_iff.2 ?_⟩ @@ -578,24 +579,24 @@ theorem of_restrictScalars_finite (R A M : Type*) [CommSemiring R] [Semiring A] variable {R M} -instance prod [hM : Finite R M] [hN : Finite R N] : Finite R (M × N) := +instance prod [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (M × N) := ⟨by rw [← Submodule.prod_top] exact hM.1.prod hN.1⟩ instance pi {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCommMonoid (M i)] - [∀ i, Module R (M i)] [h : ∀ i, Finite R (M i)] : Finite R (∀ i, M i) := + [∀ i, Module R (M i)] [h : ∀ i, Module.Finite R (M i)] : Module.Finite R (∀ i, M i) := ⟨by rw [← Submodule.pi_top] exact Submodule.fg_pi fun i => (h i).1⟩ -theorem equiv [Finite R M] (e : M ≃ₗ[R] N) : Finite R N := +theorem equiv [Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N := of_surjective (e : M →ₗ[R] N) e.surjective -theorem equiv_iff (e : M ≃ₗ[R] N) : Finite R M ↔ Finite R N := +theorem equiv_iff (e : M ≃ₗ[R] N) : Module.Finite R M ↔ Module.Finite R N := ⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩ -instance ulift [Finite R M] : Finite R (ULift M) := equiv ULift.moduleEquiv.symm +instance ulift [Module.Finite R M] : Module.Finite R (ULift M) := equiv ULift.moduleEquiv.symm theorem iff_fg {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans (fg_top _) @@ -603,7 +604,7 @@ variable (R M) instance bot : Module.Finite R (⊥ : Submodule R M) := iff_fg.mpr fg_bot -instance top [Finite R M] : Module.Finite R (⊤ : Submodule R M) := iff_fg.mpr out +instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := iff_fg.mpr out variable {M} @@ -642,7 +643,7 @@ section Algebra theorem trans {R : Type*} (A M : Type*) [Semiring R] [Semiring A] [Module R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] : - ∀ [Finite R A] [Finite A M], Finite R M + ∀ [Module.Finite R A] [Module.Finite A M], Module.Finite R M | ⟨⟨s, hs⟩⟩, ⟨⟨t, ht⟩⟩ => ⟨Submodule.fg_def.2 ⟨Set.image2 (· • ·) (↑s : Set A) (↑t : Set M), diff --git a/Mathlib/RingTheory/Flat/EquationalCriterion.lean b/Mathlib/RingTheory/Flat/EquationalCriterion.lean index e90cd0987d45c..763d9dc2c83db 100644 --- a/Mathlib/RingTheory/Flat/EquationalCriterion.lean +++ b/Mathlib/RingTheory/Flat/EquationalCriterion.lean @@ -120,8 +120,8 @@ theorem tfae_equational_criterion : List.TFAE [ ∀ {ι : Type u} [Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (_ : Fintype κ) (a : (ι →₀ R) →ₗ[R] (κ →₀ R)) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0, - ∀ {N : Type u} [AddCommGroup N] [Module R N] [Free R N] [Finite R N] {f : N} {x : N →ₗ[R] M}, - x f = 0 → + ∀ {N : Type u} [AddCommGroup N] [Module R N] [Free R N] [Module.Finite R N] {f : N} + {x : N →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (_ : Fintype κ) (a : N →ₗ[R] (κ →₀ R)) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0] := by classical @@ -243,8 +243,8 @@ Let $M$ be a flat module over a commutative ring $R$. Let $N$ be a finite free m let $f \in N$, and let $x \colon N \to M$ be a homomorphism such that $x(f) = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. -/ -theorem exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type u} - [AddCommGroup N] [Module R N] [Free R N] [Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) : +theorem exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type u} [AddCommGroup N] + [Module R N] [Free R N] [Module.Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) : ∃ (κ : Type u) (_ : Fintype κ) (a : N →ₗ[R] (κ →₀ R)) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0 := by exact ((tfae_equational_criterion R M).out 0 5 rfl rfl).mp ‹Flat R M› h @@ -254,8 +254,8 @@ free, and let $f \colon K \to N$ and $x \colon N \to M$ be homomorphisms such th $x \circ f = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a \circ f = 0$. -/ -theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type u} - [AddCommGroup K] [Module R K] [Finite R K] [AddCommGroup N] [Module R N] [Free R N] [Finite R N] +theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type u} [AddCommGroup K] + [Module R K] [Module.Finite R K] [AddCommGroup N] [Module R N] [Free R N] [Module.Finite R N] {f : K →ₗ[R] N} {x : N →ₗ[R] M} (h : x ∘ₗ f = 0) : ∃ (κ : Type u) (_ : Fintype κ) (a : N →ₗ[R] (κ →₀ R)) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a ∘ₗ f = 0 := by @@ -283,7 +283,7 @@ theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type u} [Add ∃ (κ : Type u) (_ : Fintype κ) (h₂ : P →ₗ[R] (κ →₀ R)) (h₃ : (κ →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂ := by obtain ⟨L, _, _, K, ϕ, _, _, hK⟩ := FinitePresentation.equiv_quotient R P - haveI : Finite R ↥K := Module.Finite.iff_fg.mpr hK + haveI : Module.Finite R ↥K := Module.Finite.iff_fg.mpr hK have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero] obtain ⟨κ, hκ, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free this diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 948ea0ff4843f..9ce01fea0e26b 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -251,7 +251,7 @@ lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maxima · simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span] · exact Ideal.Quotient.mk_surjective -open FiniteDimensional +open Module lemma finrank_cotangentSpace_eq_zero_iff [IsNoetherianRing R] : finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R := by diff --git a/Mathlib/RingTheory/LittleWedderburn.lean b/Mathlib/RingTheory/LittleWedderburn.lean index 24f9b1cce5f40..42f44f6d9f529 100644 --- a/Mathlib/RingTheory/LittleWedderburn.lean +++ b/Mathlib/RingTheory/LittleWedderburn.lean @@ -48,7 +48,7 @@ private def InductionHyp : Prop := namespace InductionHyp -open FiniteDimensional Polynomial +open Module Polynomial variable {D} diff --git a/Mathlib/RingTheory/LocalRing/Module.lean b/Mathlib/RingTheory/LocalRing/Module.lean index 06103c98b607e..838c66b8f3863 100644 --- a/Mathlib/RingTheory/LocalRing/Module.lean +++ b/Mathlib/RingTheory/LocalRing/Module.lean @@ -171,12 +171,12 @@ theorem free_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M] refine ⟨?_, this⟩ rw [← LinearMap.ker_eq_bot (M := k ⊗[R] (I →₀ R)) (f := i.baseChange k), ← Submodule.finrank_eq_zero (R := k) (M := k ⊗[R] (I →₀ R)), - ← Nat.add_right_inj (n := FiniteDimensional.finrank k (LinearMap.range <| i.baseChange k)), + ← Nat.add_right_inj (n := Module.finrank k (LinearMap.range <| i.baseChange k)), LinearMap.finrank_range_add_finrank_ker (V := k ⊗[R] (I →₀ R)), LinearMap.range_eq_top.mpr this, finrank_top] - simp only [FiniteDimensional.finrank_tensorProduct, FiniteDimensional.finrank_self, - FiniteDimensional.finrank_finsupp_self, one_mul, add_zero] - rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex] + simp only [Module.finrank_tensorProduct, Module.finrank_self, + Module.finrank_finsupp_self, one_mul, add_zero] + rw [Module.finrank_eq_card_chooseBasisIndex] -- On the other hand, `m ⊗ M → M` injective => `Tor₁(k, M) = 0` => `k ⊗ ker(i) → kᴵ` injective. have := @lTensor_injective_of_exact_of_exact_of_rTensor_injective (N₁ := LinearMap.ker i) (N₂ := I →₀ R) (N₃ := M) diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean index f3e0b396a8eb4..3cf506b139773 100644 --- a/Mathlib/RingTheory/Noetherian.lean +++ b/Mathlib/RingTheory/Noetherian.lean @@ -145,17 +145,17 @@ variable [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R variable (R M) -- see Note [lower instance priority] -instance (priority := 100) IsNoetherian.finite [IsNoetherian R M] : Finite R M := +instance (priority := 100) IsNoetherian.finite [IsNoetherian R M] : Module.Finite R M := ⟨IsNoetherian.noetherian ⊤⟩ instance {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] - [IsNoetherian R₁ S] (I : Ideal S) : Finite R₁ I := + [IsNoetherian R₁ S] (I : Ideal S) : Module.Finite R₁ I := IsNoetherian.finite R₁ ((I : Submodule S S).restrictScalars R₁) variable {R M} theorem Finite.of_injective [IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective f) : - Finite R M := + Module.Finite R M := ⟨fg_of_injective f hf⟩ end Module diff --git a/Mathlib/RingTheory/Norm/Basic.lean b/Mathlib/RingTheory/Norm/Basic.lean index 142c31df3e1f0..e58b1fc23e208 100644 --- a/Mathlib/RingTheory/Norm/Basic.lean +++ b/Mathlib/RingTheory/Norm/Basic.lean @@ -46,7 +46,7 @@ variable {K L F : Type*} [Field K] [Field L] [Field F] variable [Algebra K L] [Algebra K F] variable {ι : Type w} -open FiniteDimensional +open Module open LinearMap @@ -153,7 +153,7 @@ theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_one {x : L} (hx : ¬Is contrapose! hx obtain ⟨s, ⟨b⟩⟩ := hx refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_ - · exact (Submodule.fg_iff_finiteDimensional _).mpr (of_fintype_basis b) + · exact (Submodule.fg_iff_finiteDimensional _).mpr (.of_fintype_basis b) · exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x) theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots (x : L) diff --git a/Mathlib/RingTheory/Norm/Defs.lean b/Mathlib/RingTheory/Norm/Defs.lean index 6f1c21fae5c00..b7f2ce47f5c97 100644 --- a/Mathlib/RingTheory/Norm/Defs.lean +++ b/Mathlib/RingTheory/Norm/Defs.lean @@ -41,7 +41,7 @@ variable {K L F : Type*} [Field K] [Field L] [Field F] variable [Algebra K L] [Algebra K F] variable {ι : Type w} -open FiniteDimensional +open Module open LinearMap diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean index a7f446664bdad..6365d391b724f 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean @@ -137,7 +137,7 @@ theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {B : Pow letI := B.finite let P := minpoly R B.gen obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne' - have finrank_K_L : FiniteDimensional.finrank K L = B.dim := B.finrank + have finrank_K_L : Module.finrank K L = B.dim := B.finrank have deg_K_P : (minpoly K B.gen).natDegree = B.dim := B.natDegree_minpoly have deg_R_P : P.natDegree = B.dim := by rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, diff --git a/Mathlib/RingTheory/PowerBasis.lean b/Mathlib/RingTheory/PowerBasis.lean index b0b9c2d3d7536..a9cf86b0049c1 100644 --- a/Mathlib/RingTheory/PowerBasis.lean +++ b/Mathlib/RingTheory/PowerBasis.lean @@ -19,7 +19,7 @@ gives a `PowerBasis` structure generated by `x`. * `PowerBasis R A`: a structure containing an `x` and an `n` such that `1, x, ..., x^n` is a basis for the `R`-algebra `A` (viewed as an `R`-module). -* `finrank (hf : f ≠ 0) : FiniteDimensional.finrank K (AdjoinRoot f) = f.natDegree`, +* `finrank (hf : f ≠ 0) : Module.finrank K (AdjoinRoot f) = f.natDegree`, the dimension of `AdjoinRoot f` equals the degree of `f` * `PowerBasis.lift (pb : PowerBasis R S)`: if `y : S'` satisfies the same @@ -77,8 +77,8 @@ theorem finite (pb : PowerBasis R S) : Module.Finite R S := .of_basis pb.basis @[deprecated (since := "2024-03-05")] alias finiteDimensional := PowerBasis.finite theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) : - FiniteDimensional.finrank R S = pb.dim := by - rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin] + Module.finrank R S = pb.dim := by + rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin] theorem mem_span_pow' {x y : S} {d : ℕ} : y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔ diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 5bc001188d6d1..86e5d7e807588 100644 --- a/Mathlib/RingTheory/SimpleModule.lean +++ b/Mathlib/RingTheory/SimpleModule.lean @@ -163,7 +163,7 @@ theorem isSimpleModule_self_iff_isUnit : exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩ theorem isSimpleModule_iff_finrank_eq_one {R} [DivisionRing R] [Module R M] : - IsSimpleModule R M ↔ FiniteDimensional.finrank R M = 1 := + IsSimpleModule R M ↔ Module.finrank R M = 1 := ⟨fun h ↦ have := h.nontrivial; have ⟨v, hv⟩ := exists_ne (0 : M) (finrank_eq_one_iff_of_nonzero' v hv).mpr (IsSimpleModule.toSpanSingleton_surjective R hv), is_simple_module_of_finrank_eq_one⟩ diff --git a/Mathlib/RingTheory/Trace/Basic.lean b/Mathlib/RingTheory/Trace/Basic.lean index 6690ed277ff91..e06b0141ff923 100644 --- a/Mathlib/RingTheory/Trace/Basic.lean +++ b/Mathlib/RingTheory/Trace/Basic.lean @@ -47,7 +47,7 @@ variable [Algebra R S] [Algebra R T] variable {K L : Type*} [Field K] [Field L] [Algebra K L] variable {ι κ : Type w} [Fintype ι] -open FiniteDimensional +open Module open LinearMap (BilinForm) open LinearMap @@ -435,7 +435,7 @@ variable (K L) theorem traceForm_nondegenerate [FiniteDimensional K L] [Algebra.IsSeparable K L] : (traceForm K L).Nondegenerate := BilinForm.nondegenerate_of_det_ne_zero (traceForm K L) _ - (det_traceForm_ne_zero (FiniteDimensional.finBasis K L)) + (det_traceForm_ne_zero (Module.finBasis K L)) theorem Algebra.trace_ne_zero [FiniteDimensional K L] [Algebra.IsSeparable K L] : Algebra.trace K L ≠ 0 := by diff --git a/Mathlib/RingTheory/Trace/Defs.lean b/Mathlib/RingTheory/Trace/Defs.lean index 86218f0b3ecff..8d961bf7c82e6 100644 --- a/Mathlib/RingTheory/Trace/Defs.lean +++ b/Mathlib/RingTheory/Trace/Defs.lean @@ -48,7 +48,7 @@ variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] variable [Algebra R S] [Algebra R T] variable {ι κ : Type w} [Fintype ι] -open FiniteDimensional +open Module open LinearMap (BilinForm) open LinearMap diff --git a/Mathlib/RingTheory/Valuation/Minpoly.lean b/Mathlib/RingTheory/Valuation/Minpoly.lean index 3448962da4e70..00094cc933c86 100644 --- a/Mathlib/RingTheory/Valuation/Minpoly.lean +++ b/Mathlib/RingTheory/Valuation/Minpoly.lean @@ -21,7 +21,7 @@ Let `K` be a field with a valuation `v` and let `L` be a field extension of `K`. is helpful for defining the valuation on `L` inducing `v`. -/ -open FiniteDimensional minpoly Polynomial +open Module minpoly Polynomial variable {K : Type*} [Field K] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) (L : Type*) [Field L] [Algebra K L] diff --git a/Mathlib/RingTheory/WittVector/Isocrystal.lean b/Mathlib/RingTheory/WittVector/Isocrystal.lean index 5ba7feb02f7c6..0f5d266cc6c93 100644 --- a/Mathlib/RingTheory/WittVector/Isocrystal.lean +++ b/Mathlib/RingTheory/WittVector/Isocrystal.lean @@ -54,7 +54,7 @@ This file introduces notation in the locale `Isocrystal`. noncomputable section -open FiniteDimensional +open Module namespace WittVector @@ -181,7 +181,7 @@ admits an isomorphism to one of the standard (indexed by `m : ℤ`) one-dimensio theorem isocrystal_classification (k : Type*) [Field k] [IsAlgClosed k] [CharP k p] (V : Type*) [AddCommGroup V] [Isocrystal p k V] (h_dim : finrank K(p, k) V = 1) : ∃ m : ℤ, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V) := by - haveI : Nontrivial V := FiniteDimensional.nontrivial_of_finrank_eq_succ h_dim + haveI : Nontrivial V := Module.nontrivial_of_finrank_eq_succ h_dim obtain ⟨x, hx⟩ : ∃ x : V, x ≠ 0 := exists_ne 0 have : Φ(p, k) x ≠ 0 := by simpa only [map_zero] using Φ(p, k).injective.ne hx obtain ⟨a, ha, hax⟩ : ∃ a : K(p, k), a ≠ 0 ∧ Φ(p, k) x = a • x := by diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 31b45d485cdb9..3c7e1401aa012 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -47,7 +47,7 @@ universe u v w x noncomputable section -open Set FiniteDimensional TopologicalSpace Filter +open Filter Module Set TopologicalSpace section Field @@ -197,7 +197,7 @@ private theorem continuous_equivFun_basis_aux [T2Space E] {ι : Type v} [Fintype induction' hn : Fintype.card ι with n IH generalizing ι E · rw [Fintype.card_eq_zero_iff] at hn exact continuous_of_const fun x y => funext hn.elim - · haveI : FiniteDimensional 𝕜 E := of_fintype_basis ξ + · haveI : FiniteDimensional 𝕜 E := .of_fintype_basis ξ -- first step: thanks to the induction hypothesis, any n-dimensional subspace is equivalent -- to a standard space of dimension n, hence it is complete and therefore closed. have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by @@ -264,7 +264,7 @@ continuous (see `LinearMap.continuous_of_finiteDimensional`), which in turn impl norms are equivalent in finite dimensions. -/ theorem continuous_equivFun_basis [T2Space E] {ι : Type*} [Finite ι] (ξ : Basis ι 𝕜 E) : Continuous ξ.equivFun := - haveI : FiniteDimensional 𝕜 E := of_fintype_basis ξ + haveI : FiniteDimensional 𝕜 E := .of_fintype_basis ξ ξ.equivFun.toLinearMap.continuous_of_finiteDimensional namespace LinearMap diff --git a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean index 1018155f553a7..46a5798a92a07 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean @@ -84,7 +84,7 @@ Hausdorff measure, Hausdorff dimension, dimension open scoped MeasureTheory ENNReal NNReal Topology -open MeasureTheory MeasureTheory.Measure Set TopologicalSpace FiniteDimensional Filter +open MeasureTheory MeasureTheory.Measure Set TopologicalSpace Module Filter variable {ι X Y : Type*} [EMetricSpace X] [EMetricSpace Y] @@ -441,7 +441,7 @@ theorem dimH_univ_pi_fin (n : ℕ) : dimH (univ : Set (Fin n → ℝ)) = n := by theorem dimH_of_mem_nhds {x : E} {s : Set E} (h : s ∈ 𝓝 x) : dimH s = finrank ℝ E := by have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := - ContinuousLinearEquiv.ofFinrankEq (FiniteDimensional.finrank_fin_fun ℝ).symm + ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm rw [← e.dimH_image] refine le_antisymm ?_ ?_ · exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _) @@ -459,7 +459,7 @@ theorem dimH_univ_eq_finrank : dimH (univ : Set E) = finrank ℝ E := dimH_of_mem_nhds (@univ_mem _ (𝓝 0)) theorem dimH_univ : dimH (univ : Set ℝ) = 1 := by - rw [dimH_univ_eq_finrank ℝ, FiniteDimensional.finrank_self, Nat.cast_one] + rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one] variable {E}