From 9f94180e61834f63bcc64179618ebfa4ab2204d2 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 27 May 2023 14:37:51 +0000 Subject: [PATCH] chore: tidy various files (#4423) --- .../Algebra/Category/GroupCat/Colimits.lean | 12 +-- Mathlib/Algebra/Category/GroupCat/Images.lean | 2 +- .../Algebra/Category/Ring/Constructions.lean | 34 ++++----- Mathlib/Algebra/Module/Torsion.lean | 9 +-- .../PrimeSpectrum/IsOpenComapC.lean | 6 +- Mathlib/AlgebraicGeometry/SheafedSpace.lean | 15 +--- .../BoxIntegral/Partition/Additive.lean | 16 ++-- .../Analysis/NormedSpace/Star/Multiplier.lean | 18 ++--- Mathlib/Combinatorics/Configuration.lean | 8 +- Mathlib/Data/Nat/Squarefree.lean | 18 ++--- Mathlib/FieldTheory/Separable.lean | 20 ++--- .../GroupTheory/SpecificGroups/Cyclic.lean | 76 +++++++++---------- Mathlib/LinearAlgebra/Contraction.lean | 3 +- .../Matrix/GeneralLinearGroup.lean | 12 +-- Mathlib/RingTheory/IntegralDomain.lean | 22 ++---- Mathlib/RingTheory/LaurentSeries.lean | 27 +++---- .../LocalizationLocalization.lean | 9 +-- 17 files changed, 127 insertions(+), 180 deletions(-) diff --git a/Mathlib/Algebra/Category/GroupCat/Colimits.lean b/Mathlib/Algebra/Category/GroupCat/Colimits.lean index 7338579302f43..3ff2ec504fe3e 100644 --- a/Mathlib/Algebra/Category/GroupCat/Colimits.lean +++ b/Mathlib/Algebra/Category/GroupCat/Colimits.lean @@ -16,12 +16,12 @@ import Mathlib.CategoryTheory.ConcreteCategory.Elementwise /-! # The category of additive commutative groups has all colimits. -This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`. +This file uses a "pre-automated" approach, just as for `Mon/Colimits.lean`. It is a very uniform approach, that conceivably could be synthesised directly -by a tactic that analyses the shape of `add_comm_group` and `monoid_hom`. +by a tactic that analyses the shape of `AddCommGroup` and `MonoidHom`. TODO: -In fact, in `AddCommGroup` there is a much nicer model of colimits as quotients +In fact, in `AddCommGroupCat` there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead). -/ @@ -40,7 +40,7 @@ open CategoryTheory.Limits namespace AddCommGroupCat.Colimits /-! -We build the colimit of a diagram in `AddCommGroup` by constructing the +We build the colimit of a diagram in `AddCommGroupCat` by constructing the free group on the disjoint union of all the abelian groups in the diagram, then taking the quotient by the abelian group laws within each abelian group, and the identifications given by the morphisms in the diagram. @@ -105,7 +105,7 @@ def colimitSetoid : Setoid (Prequotient F) where attribute [instance] colimitSetoid -/-- The underlying type of the colimit of a diagram in `AddCommGroup`. +/-- The underlying type of the colimit of a diagram in `AddCommGroupCat`. -/ def ColimitType : Type v := Quotient (colimitSetoid F) @@ -306,7 +306,7 @@ namespace AddCommGroupCat open QuotientAddGroup -/-- The categorical cokernel of a morphism in `AddCommGroup` +/-- The categorical cokernel of a morphism in `AddCommGroupCat` agrees with the usual group-theoretical quotient. -/ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H) : diff --git a/Mathlib/Algebra/Category/GroupCat/Images.lean b/Mathlib/Algebra/Category/GroupCat/Images.lean index 71e7ff75f2f9d..0b9b726bd3a0c 100644 --- a/Mathlib/Algebra/Category/GroupCat/Images.lean +++ b/Mathlib/Algebra/Category/GroupCat/Images.lean @@ -37,7 +37,7 @@ attribute [local ext] Subtype.ext_val section --- implementation details of `has_image` for `AddCommGroupCat`; use the API, not these +-- implementation details of `IsImage` for `AddCommGroupCat`; use the API, not these /-- the image of a morphism in `AddCommGroupCat` is just the bundling of `AddMonoidHom.range f` -/ def image : AddCommGroupCat := AddCommGroupCat.of (AddMonoidHom.range f) diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean index e2f488765f073..84bf7d558e298 100644 --- a/Mathlib/Algebra/Category/Ring/Constructions.lean +++ b/Mathlib/Algebra/Category/Ring/Constructions.lean @@ -16,23 +16,21 @@ import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial import Mathlib.RingTheory.Subring.Basic /-! -# Constructions of (co)limits in CommRing +# Constructions of (co)limits in `CommRingCat` -In this file we provide the explicit (co)cones for various (co)limits in `CommRing`, including +In this file we provide the explicit (co)cones for various (co)limits in `CommRingCat`, including * tensor product is the pushout * `Z` is the initial object * `0` is the strict terminal object * cartesian product is the product -* `ring_hom.eq_locus` is the equalizer +* `RingHom.eqLocus` is the equalizer -/ universe u u' -open CategoryTheory CategoryTheory.Limits - -open TensorProduct +open CategoryTheory CategoryTheory.Limits TensorProduct namespace CommRingCat @@ -40,7 +38,7 @@ section Pushout variable {R A B : CommRingCat.{u}} (f : R ⟶ A) (g : R ⟶ B) -/-- The explicit cocone with tensor products as the fibered product in `CommRing`. -/ +/-- The explicit cocone with tensor products as the fibered product in `CommRingCat`. -/ def pushoutCocone : Limits.PushoutCocone f g := by letI := RingHom.toAlgebra f letI := RingHom.toAlgebra g @@ -148,12 +146,12 @@ end Pushout section Terminal -/-- The trivial ring is the (strict) terminal object of `CommRing`. -/ +/-- The trivial ring is the (strict) terminal object of `CommRingCat`. -/ def punitIsTerminal : IsTerminal (CommRingCat.of.{u} PUnit) := by refine IsTerminal.ofUnique (h := fun X => ⟨⟨⟨⟨1, rfl⟩, fun _ _ => rfl⟩, ?_, ?_⟩, ?_⟩) - . dsimp - . intros; dsimp - . intros f; ext; rfl + · dsimp + · intros; dsimp + · intros f; ext; rfl set_option linter.uppercaseLean3 false in #align CommRing.punit_is_terminal CommRingCat.punitIsTerminal @@ -177,7 +175,7 @@ theorem subsingleton_of_isTerminal {X : CommRingCat} (hX : IsTerminal X) : Subsi set_option linter.uppercaseLean3 false in #align CommRing.subsingleton_of_is_terminal CommRingCat.subsingleton_of_isTerminal -/-- `ℤ` is the initial object of `CommRing`. -/ +/-- `ℤ` is the initial object of `CommRingCat`. -/ def zIsInitial : IsInitial (CommRingCat.of ℤ) := IsInitial.ofUnique (h := fun R => ⟨⟨Int.castRingHom R⟩, fun a => a.ext_int _⟩) set_option linter.uppercaseLean3 false in @@ -189,14 +187,14 @@ section Product variable (A B : CommRingCat.{u}) -/-- The product in `CommRing` is the cartesian product. This is the binary fan. -/ +/-- The product in `CommRingCat` is the cartesian product. This is the binary fan. -/ @[simps! pt] def prodFan : BinaryFan A B := BinaryFan.mk (CommRingCat.ofHom <| RingHom.fst A B) (CommRingCat.ofHom <| RingHom.snd A B) set_option linter.uppercaseLean3 false in #align CommRing.prod_fan CommRingCat.prodFan -/-- The product in `CommRing` is the cartesian product. -/ +/-- The product in `CommRingCat` is the cartesian product. -/ def prodFanIsLimit : IsLimit (prodFan A B) where lift c := RingHom.prod (c.π.app ⟨WalkingPair.left⟩) (c.π.app ⟨WalkingPair.right⟩) fac c j := by @@ -223,7 +221,7 @@ section Equalizer variable {A B : CommRingCat.{u}} (f g : A ⟶ B) -/-- The equalizer in `CommRing` is the equalizer as sets. This is the equalizer fork. -/ +/-- The equalizer in `CommRingCat` is the equalizer as sets. This is the equalizer fork. -/ def equalizerFork : Fork f g := Fork.ofι (CommRingCat.ofHom (RingHom.eqLocus f g).subtype) <| by ext ⟨x, e⟩ @@ -231,7 +229,7 @@ def equalizerFork : Fork f g := set_option linter.uppercaseLean3 false in #align CommRing.equalizer_fork CommRingCat.equalizerFork -/-- The equalizer in `CommRing` is the equalizer as sets. -/ +/-- The equalizer in `CommRingCat` is the equalizer as sets. -/ def equalizerForkIsLimit : IsLimit (equalizerFork f g) := by fapply Fork.IsLimit.mk' intro s @@ -291,8 +289,8 @@ end Equalizer section Pullback -/-- In the category of `CommRing`, the pullback of `f : A ⟶ C` and `g : B ⟶ C` is the `eq_locus` of -the two maps `A × B ⟶ C`. This is the constructed pullback cone. +/-- In the category of `CommRingCat`, the pullback of `f : A ⟶ C` and `g : B ⟶ C` is the `eqLocus` +of the two maps `A × B ⟶ C`. This is the constructed pullback cone. -/ def pullbackCone {A B C : CommRingCat.{u}} (f : A ⟶ C) (g : B ⟶ C) : PullbackCone f g := PullbackCone.mk diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index e79a40e8dde1f..946013952fbc3 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -30,9 +30,9 @@ import Mathlib.RingTheory.Finiteness * `Submodule.torsion R M` : the torsion submoule, containing all elements `x` of `M` such that `a • x = 0` for some non-zero-divisor `a` in `R`. * `Module.IsTorsionBy R M a` : the property that defines a `a`-torsion module. Similarly, - `is_torsion_by_set`, `is_torsion'` and `is_torsion`. + `IsTorsionBySet`, `IsTorsion'` and `IsTorsion`. * `Module.IsTorsionBySet.module` : Creates a `R ⧸ I`-module from a `R`-module that - `is_torsion_by_set R _ I`. + `IsTorsionBySet R _ I`. ## Main statements @@ -46,7 +46,7 @@ import Mathlib.RingTheory.Finiteness `p i`-torsion submodules when the `p i` are pairwise coprime. A more general version with coprime ideals is `Submodule.torsionBySet_is_internal`. * `Submodule.noZeroSMulDivisors_iff_torsion_bot` : a module over a domain has - `no_zero_smul_divisors` (that is, there is no non-zero `a`, `x` such that `a • x = 0`) + `NoZeroSMulDivisors` (that is, there is no non-zero `a`, `x` such that `a • x = 0`) iff its torsion submodule is trivial. * `Submodule.QuotientTorsion.torsion_eq_bot` : quotienting by the torsion submodule makes the torsion submodule of the new module trivial. If `R` is a domain, we can derive an instance @@ -54,7 +54,7 @@ import Mathlib.RingTheory.Finiteness ## Notation -* The notions are defined for a `comm_semiring R` and a `module R M`. Some additional hypotheses on +* The notions are defined for a `CommSemiring R` and a `Module R M`. Some additional hypotheses on `R` and `M` are required by some lemmas. * The letters `a`, `b`, ... are used for scalars (in `R`), while `x`, `y`, ... are used for vectors (in `M`). @@ -851,4 +851,3 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] : #align add_monoid.is_torsion_iff_is_torsion_int AddMonoid.isTorsion_iff_isTorsion_int end AddMonoid - diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean index ef07b2e0ae2c0..8741ec2dca0d8 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean @@ -22,8 +22,6 @@ https://stacks.math.columbia.edu/tag/00FB open Ideal Polynomial PrimeSpectrum Set -open Polynomial - namespace AlgebraicGeometry namespace Polynomial @@ -76,13 +74,13 @@ Stacks Project "Lemma 00FB", first part. https://stacks.math.columbia.edu/tag/00FB -/ -theorem isOpenMap_comap_c : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X])) := by +theorem isOpenMap_comap_C : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X])) := by rintro U ⟨s, z⟩ rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter, image_iUnion] simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus] exact isOpen_iUnion fun f => isOpen_imageOfDf -#align algebraic_geometry.polynomial.is_open_map_comap_C AlgebraicGeometry.Polynomial.isOpenMap_comap_c +#align algebraic_geometry.polynomial.is_open_map_comap_C AlgebraicGeometry.Polynomial.isOpenMap_comap_C end Polynomial diff --git a/Mathlib/AlgebraicGeometry/SheafedSpace.lean b/Mathlib/AlgebraicGeometry/SheafedSpace.lean index 0dacd598243a7..f81ba8e76eede 100644 --- a/Mathlib/AlgebraicGeometry/SheafedSpace.lean +++ b/Mathlib/AlgebraicGeometry/SheafedSpace.lean @@ -24,17 +24,8 @@ presheaves. universe v u -open CategoryTheory - -open TopCat - -open TopologicalSpace - -open Opposite - -open CategoryTheory.Limits - -open CategoryTheory.Category CategoryTheory.Functor +open CategoryTheory TopCat TopologicalSpace Opposite CategoryTheory.Limits CategoryTheory.Category + CategoryTheory.Functor variable (C : Type u) [Category.{v} C] @@ -69,7 +60,7 @@ set_option linter.uppercaseLean3 false in -- theorem as_coe (X : SheafedSpace.{v} C) : X.carrier = (X : TopCat.{v}) := -- rfl -- set_option linter.uppercaseLean3 false in --- #align algebraic_geometry.SheafedSpace.as_coe AlgebraicGeometry.SheafedSpace.as_coe +#noalign algebraic_geometry.SheafedSpace.as_coe -- Porting note : this gives a `simpVarHead` error (`LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.`). -- so removed @[simp] diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean index 095035e9cc971..418f7f94f4a1b 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Additive.lean @@ -34,9 +34,7 @@ rectangular box, additive function noncomputable section -open Classical BigOperators - -open Function Set +open Classical BigOperators Function Set namespace BoxIntegral @@ -175,21 +173,21 @@ theorem sum_boxes_congr [Finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI] #align box_integral.box_additive_map.sum_boxes_congr BoxIntegral.BoxAdditiveMap.sum_boxes_congr -section ToSmul +section ToSMul variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] /-- If `f` is a box-additive map, then so is the map sending `I` to the scalar multiplication by `f I` as a continuous linear map from `E` to itself. -/ -def toSmul (f : ι →ᵇᵃ[I₀] ℝ) : ι →ᵇᵃ[I₀] E →L[ℝ] E := +def toSMul (f : ι →ᵇᵃ[I₀] ℝ) : ι →ᵇᵃ[I₀] E →L[ℝ] E := f.map (ContinuousLinearMap.lsmul ℝ ℝ).toLinearMap.toAddMonoidHom -#align box_integral.box_additive_map.to_smul BoxIntegral.BoxAdditiveMap.toSmul +#align box_integral.box_additive_map.to_smul BoxIntegral.BoxAdditiveMap.toSMul @[simp] -theorem toSmul_apply (f : ι →ᵇᵃ[I₀] ℝ) (I : Box ι) (x : E) : f.toSmul I x = f I • x := rfl -#align box_integral.box_additive_map.to_smul_apply BoxIntegral.BoxAdditiveMap.toSmul_apply +theorem toSMul_apply (f : ι →ᵇᵃ[I₀] ℝ) (I : Box ι) (x : E) : f.toSMul I x = f I • x := rfl +#align box_integral.box_additive_map.to_smul_apply BoxIntegral.BoxAdditiveMap.toSMul_apply -end ToSmul +end ToSMul /-- Given a box `I₀` in `ℝⁿ⁺¹`, `f x : Box (Fin n) → G` is a family of functions indexed by a real `x` and for `x ∈ [I₀.lower i, I₀.upper i]`, `f x` is box-additive on subboxes of the `i`-th face of diff --git a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean index 90a3daf4af51e..ab4f4646f12dc 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean @@ -60,9 +60,7 @@ separately. -/ -open NNReal ENNReal - -open NNReal ContinuousLinearMap MulOpposite +open NNReal ENNReal ContinuousLinearMap MulOpposite universe u v @@ -87,7 +85,9 @@ open MultiplierAlgebra lemma DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : 𝓜(𝕜, A)) (h : a.toProd = b.toProd) : a = b := by - cases a; cases b; simpa using h + cases a + cases b + simpa using h namespace DoubleCentralizer @@ -185,8 +185,8 @@ end Scalars instance instOne : One 𝓜(𝕜, A) := ⟨⟨1, fun _x _y => rfl⟩⟩ -instance instMul : Mul 𝓜(𝕜, A) - where mul a b := +instance instMul : Mul 𝓜(𝕜, A) where + mul a b := { toProd := (a.fst.comp b.fst, b.snd.comp a.snd) central := fun x y => show b.snd (a.snd x) * y = x * a.fst (b.fst y) by simp only [central] } @@ -327,7 +327,7 @@ theorem pow_snd (n : ℕ) (a : 𝓜(𝕜, A)) : (a ^ n).snd = a.snd ^ n := rfl #align double_centralizer.pow_snd DoubleCentralizer.pow_snd -/-- The natural injection from `double_centralizer.to_prod` except the second coordinate inherits +/-- The natural injection from `DoubleCentralizer.toProd` except the second coordinate inherits `MulOpposite.op`. The ring structure on `𝓜(𝕜, A)` is the pullback under this map. -/ def toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ := fun a => (a.fst, MulOpposite.op a.snd) @@ -376,7 +376,7 @@ def toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜] #align double_centralizer.to_prod_mul_opposite_hom DoubleCentralizer.toProdMulOppositeHom /-- The module structure is inherited as the pullback under the additive group monomorphism -`double_centralizer.to_prod : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)` -/ +`DoubleCentralizer.toProd : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)` -/ instance instModule {S : Type _} [Semiring S] [Module S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] : Module S 𝓜(𝕜, A) := Function.Injective.module S toProdHom (ext (𝕜 := 𝕜) (A := A)) fun _x _y => rfl @@ -424,7 +424,7 @@ section Star variable [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A] /-- The star operation on `a : 𝓜(𝕜, A)` is given by -`(star a).to_prod = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`. -/ +`(star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`. -/ instance instStar : Star 𝓜(𝕜, A) where star a := { fst := diff --git a/Mathlib/Combinatorics/Configuration.lean b/Mathlib/Combinatorics/Configuration.lean index 392f20767dc3b..677ba589be470 100644 --- a/Mathlib/Combinatorics/Configuration.lean +++ b/Mathlib/Combinatorics/Configuration.lean @@ -28,10 +28,10 @@ This file introduces abstract configurations of points and lines, and proves som * `Configuration.pointCount`: The number of lines through a given line. ## Main statements -* `Configuration.HasLines.card_le`: `has_lines` implies `|P| ≤ |L|`. -* `Configuration.HasPoints.card_le`: `has_points` implies `|L| ≤ |P|`. -* `Configuration.HasLines.hasPoints`: `has_lines` and `|P| = |L|` implies `has_points`. -* `Configuration.HasPoints.hasLines`: `has_points` and `|P| = |L|` implies `has_lines`. +* `Configuration.HasLines.card_le`: `HasLines` implies `|P| ≤ |L|`. +* `Configuration.HasPoints.card_le`: `HasPoints` implies `|L| ≤ |P|`. +* `Configuration.HasLines.hasPoints`: `HasLines` and `|P| = |L|` implies `HasPoints`. +* `Configuration.HasPoints.hasLines`: `HasPoints` and `|P| = |L|` implies `HasLines`. Together, these four statements say that any two of the following properties imply the third: (a) `HasLines`, (b) `HasPoints`, (c) `|P| = |L|`. diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 95157dfcadc87..2550231b4fb5b 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -18,7 +18,7 @@ import Mathlib.RingTheory.Int.Basic A number is squarefree when it is not divisible by any squares except the squares of units. ## Main Results - - `nat.squarefree_iff_nodup_factors`: A positive natural number `x` is squarefree iff + - `Nat.squarefree_iff_nodup_factors`: A positive natural number `x` is squarefree iff the list `factors x` has no duplicate factors. ## Tags @@ -67,10 +67,7 @@ theorem squarefree_iff_factorization_le_one {n : ℕ} (hn : n ≠ 0) : theorem Squarefree.ext_iff {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : n = m ↔ ∀ p, Prime p → (p ∣ n ↔ p ∣ m) := by - refine' - ⟨by - rintro rfl - simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => _⟩ + refine' ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => _⟩ by_cases hp : p.Prime · have h₁ := h _ hp rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff, @@ -88,10 +85,7 @@ theorem Squarefree.ext_iff {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : theorem squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) : Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1 := by - refine' - ⟨fun h => _, by - rintro ⟨hn, rfl⟩ - simpa⟩ + refine' ⟨fun h => _, by rintro ⟨hn, rfl⟩; simpa⟩ rcases eq_or_ne n 0 with (rfl | -) · simp [zero_pow hk.bot_lt] at h refine' ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => _⟩ @@ -102,7 +96,7 @@ theorem squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) : #align nat.squarefree_pow_iff Nat.squarefree_pow_iff theorem squarefree_and_prime_pow_iff_prime {n : ℕ} : Squarefree n ∧ IsPrimePow n ↔ Prime n := by - refine' Iff.symm ⟨fun hn => ⟨hn.squarefree, hn.isPrimePow⟩, _⟩ + refine' ⟨_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩ rw [isPrimePow_nat_iff] rintro ⟨h, p, k, hp, hk, rfl⟩ rw [squarefree_pow_iff hp.ne_one hk.ne'] at h @@ -127,7 +121,7 @@ termination_by _ n k => sqrt n + 2 - k #align nat.min_sq_fac_aux Nat.minSqFacAux /-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no - such `p` (that is, `n` is squarefree). See also `squarefree_iff_min_sq_fac`. -/ + such `p` (that is, `n` is squarefree). See also `Nat.squarefree_iff_minSqFac`. -/ def minSqFac (n : ℕ) : Option ℕ := if 2 ∣ n then let n' := n / 2 @@ -135,7 +129,7 @@ def minSqFac (n : ℕ) : Option ℕ := else minSqFacAux n 3 #align nat.min_sq_fac Nat.minSqFac -/-- The correctness property of the return value of `min_sq_fac`. +/-- The correctness property of the return value of `minSqFac`. * If `none`, then `n` is squarefree; * If `some d`, then `d` is a minimal square factor of `n` -/ def MinSqFacProp (n : ℕ) : Option ℕ → Prop diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index afe61c626234b..0332f0c10b37c 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -30,9 +30,7 @@ properties about separable polynomials here. universe u v w -open Classical BigOperators Polynomial - -open Finset +open Classical BigOperators Polynomial Finset namespace Polynomial @@ -164,10 +162,7 @@ theorem multiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : theorem Separable.squarefree {p : R[X]} (hsep : Separable p) : Squarefree p := by rw [multiplicity.squarefree_iff_multiplicity_le_one p] - intro f - by_cases hunit : IsUnit f - · exact Or.inr hunit - exact Or.inl (multiplicity_le_one_of_separable hunit hsep) + exact fun f => or_iff_not_imp_right.mpr fun hunit => multiplicity_le_one_of_separable hunit hsep #align polynomial.separable.squarefree Polynomial.Separable.squarefree end CommSemiring @@ -491,9 +486,9 @@ variable (F K : Type _) [CommRing F] [Ring K] [Algebra F K] -- TODO: refactor to allow transcendental extensions? -- See: https://en.wikipedia.org/wiki/Separable_extension#Separability_of_transcendental_extensions --- Note that right now a Galois extension (class `is_galois`) is defined to be an extension which +-- Note that right now a Galois extension (class `IsGalois`) is defined to be an extension which -- is separable and normal, so if the definition of separable changes here at some point --- to allow non-algebraic extensions, then the definition of `is_galois` must also be changed. +-- to allow non-algebraic extensions, then the definition of `IsGalois` must also be changed. /-- Typeclass for separable field extension: `K` is a separable field extension of `F` iff the minimal polynomial of every `x : K` is separable. @@ -501,14 +496,14 @@ We define this for general (commutative) rings and only assume `F` and `K` are f is needed for a proof. -/ class IsSeparable : Prop where - is_integral' (x : K) : IsIntegral F x + isIntegral' (x : K) : IsIntegral F x separable' (x : K) : (minpoly F x).Separable #align is_separable IsSeparable variable (F : Type _) {K : Type _} [CommRing F] [Ring K] [Algebra F K] theorem IsSeparable.isIntegral [IsSeparable F K] : ∀ x : K, IsIntegral F x := - IsSeparable.is_integral' + IsSeparable.isIntegral' #align is_separable.is_integral IsSeparable.isIntegral theorem IsSeparable.separable [IsSeparable F K] : ∀ x : K, (minpoly F x).Separable := @@ -525,7 +520,8 @@ theorem isSeparable_iff : IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ (min end CommRing instance isSeparable_self (F : Type _) [Field F] : IsSeparable F F := - ⟨fun x => isIntegral_algebraMap, fun x => by + ⟨fun x => isIntegral_algebraMap, + fun x => by rw [minpoly.eq_X_sub_C'] exact separable_X_sub_C⟩ #align is_separable_self isSeparable_self diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean index 650f796461630..7433dbd54b6d2 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean @@ -29,7 +29,7 @@ For the concrete cyclic group of order `n`, see `Data.ZMod.Basic`. ## Main statements * `isCyclic_of_prime_card` proves that a finite group of prime order is cyclic. -* `isSimpleGroup_of_prime_card`, `is_simple_group.is_cyclic`, +* `isSimpleGroup_of_prime_card`, `IsSimpleGroup.isCyclic`, and `IsSimpleGroup.prime_card` classify finite simple abelian groups. * `IsCyclic.exponent_eq_card`: For a finite cyclic group `G`, the exponent is equal to the group's cardinality. @@ -66,18 +66,18 @@ class IsCyclic (α : Type u) [Group α] : Prop where exists_generator : ∃ g : α, ∀ x, x ∈ zpowers g #align is_cyclic IsCyclic -@[to_additive is_add_cyclic_of_subsingleton] +@[to_additive isAddCyclic_of_subsingleton] instance (priority := 100) isCyclic_of_subsingleton [Group α] [Subsingleton α] : IsCyclic α := ⟨⟨1, fun x => by rw [Subsingleton.elim x 1] exact mem_zpowers 1⟩⟩ #align is_cyclic_of_subsingleton isCyclic_of_subsingleton -#align is_add_cyclic_of_subsingleton is_add_cyclic_of_subsingleton +#align is_add_cyclic_of_subsingleton isAddCyclic_of_subsingleton /-- A cyclic group is always commutative. This is not an `instance` because often we have a better proof of `CommGroup`. -/ @[to_additive - "A cyclic group is always commutative. This is not an `instance` because often we have\n + "A cyclic group is always commutative. This is not an `instance` because often we have a better proof of `AddCommGroup`."] def IsCyclic.commGroup [hg : Group α] [IsCyclic α] : CommGroup α := { hg with @@ -102,7 +102,7 @@ theorem MonoidHom.map_cyclic {G : Type _} [Group G] [h : IsCyclic G] (σ : G → #align monoid_hom.map_cyclic MonoidHom.map_cyclic #align monoid_add_hom.map_add_cyclic MonoidAddHom.map_add_cyclic -@[to_additive is_add_cyclic_of_orderOf_eq_card] +@[to_additive isAddCyclic_of_orderOf_eq_card] theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) : IsCyclic α := by classical @@ -111,16 +111,16 @@ theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fint rw [← Fintype.card_congr (Equiv.Set.univ α), orderOf_eq_card_zpowers] at hx exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx) #align is_cyclic_of_order_of_eq_card isCyclic_of_orderOf_eq_card -#align is_add_cyclic_of_order_of_eq_card is_add_cyclic_of_orderOf_eq_card +#align is_add_cyclic_of_order_of_eq_card isAddCyclic_of_orderOf_eq_card /-- A finite group of prime order is cyclic. -/ -@[to_additive is_add_cyclic_of_prime_card "A finite group of prime order is cyclic."] +@[to_additive isAddCyclic_of_prime_card "A finite group of prime order is cyclic."] theorem isCyclic_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact p.Prime] (h : Fintype.card α = p) : IsCyclic α := ⟨by obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := Fintype.exists_ne_of_one_lt_card (h.symm ▸ hp.1.one_lt) 1 classical - -- for fintype (subgroup.zpowers g) + -- for Fintype (Subgroup.zpowers g) have : Fintype.card (Subgroup.zpowers g) ∣ p := by rw [← h] apply card_subgroup_dvd_card @@ -143,7 +143,7 @@ theorem isCyclic_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [ rw [Subgroup.eq_top_of_card_eq _ that] exact Subgroup.mem_top _⟩ #align is_cyclic_of_prime_card isCyclic_of_prime_card -#align is_add_cyclic_of_prime_card is_add_cyclic_of_prime_card +#align is_add_cyclic_of_prime_card isAddCyclic_of_prime_card @[to_additive addOrderOf_eq_card_of_forall_mem_zmultiples] theorem orderOf_eq_card_of_forall_mem_zpowers [Fintype α] {g : α} (hx : ∀ x, x ∈ zpowers g) : @@ -178,13 +178,13 @@ theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers [Infinite α] {g : α} #align infinite.order_of_eq_zero_of_forall_mem_zpowers Infinite.orderOf_eq_zero_of_forall_mem_zpowers #align infinite.add_order_of_eq_zero_of_forall_mem_zmultiples Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples -@[to_additive Bot.is_add_cyclic] +@[to_additive Bot.isAddCyclic] instance Bot.isCyclic {α : Type u} [Group α] : IsCyclic (⊥ : Subgroup α) := ⟨⟨1, fun x => ⟨0, Subtype.eq <| (zpow_zero (1 : α)).trans <| Eq.symm (Subgroup.mem_bot.1 x.2)⟩⟩⟩ #align bot.is_cyclic Bot.isCyclic -#align bot.is_add_cyclic Bot.is_add_cyclic +#align bot.is_add_cyclic Bot.isAddCyclic -@[to_additive AddSubgroup.is_add_cyclic] +@[to_additive AddSubgroup.isAddCyclic] instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) : IsCyclic H := haveI := Classical.propDecidable let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α) @@ -233,7 +233,7 @@ instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup ⟨fun h => by simp at *; tauto, fun h => by rw [Subgroup.mem_bot.1 h]; exact H.one_mem⟩ subst this; infer_instance #align subgroup.is_cyclic Subgroup.isCyclic -#align add_subgroup.is_add_cyclic AddSubgroup.is_add_cyclic +#align add_subgroup.is_add_cyclic AddSubgroup.isAddCyclic open Finset Nat @@ -333,12 +333,9 @@ private theorem card_pow_eq_one_eq_orderOf_aux (a : α) : fun _ _ h => Subtype.eq (Subtype.mk.inj h)) _ = (univ.filter fun b : α => b ^ orderOf a = 1).card := Fintype.card_ofFinset _ _ ) --- Porting note: private so presumably is not used --- #align card_pow_eq_one_eq_order_of_aux card_pow_eq_one_eq_order_of_aux +-- Use φ for `Nat.totient` open Nat - --- use φ for nat.totient private theorem card_orderOf_eq_totient_aux₁ : ∀ {d : ℕ}, d ∣ Fintype.card α → @@ -364,8 +361,6 @@ private theorem card_orderOf_eq_totient_aux₁ : rw [← filter_dvd_eq_divisors hd0, sum_card_orderOf_eq_card_pow_eq_one hd0, filter_dvd_eq_divisors hd0, sum_totient, ← ha, card_pow_eq_one_eq_orderOf_aux hn a] simpa [← cons_self_properDivisors hd0, ← h1] using h2 --- Porting note: private so presumably is not used --- #align card_order_of_eq_totient_aux₁ card_order_of_eq_totient_aux₁ theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) : (univ.filter fun a : α => orderOf a = d).card = φ d := by @@ -438,18 +433,18 @@ attribute [to_additive existing IsCyclic.card_orderOf_eq_totient] @[to_additive "A finite group of prime order is simple."] theorem isSimpleGroup_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact p.Prime] (h : Fintype.card α = p) : IsSimpleGroup α := - have : Nontrivial α := by - have h' := Nat.Prime.one_lt (Fact.out (p := p.Prime)) - rw [← h] at h' - exact Fintype.one_lt_card_iff_nontrivial.1 h' - ⟨ fun H _ => by - classical - have hcard := card_subgroup_dvd_card H - rw [h, dvd_prime (Fact.out (p := p.Prime))] at hcard - refine' hcard.imp (fun h1 => _) fun hp => _ - · haveI := Fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1) - apply eq_bot_of_subsingleton - · exact eq_top_of_card_eq _ (hp.trans h.symm)⟩ + have : Nontrivial α := by + have h' := Nat.Prime.one_lt (Fact.out (p := p.Prime)) + rw [← h] at h' + exact Fintype.one_lt_card_iff_nontrivial.1 h' + ⟨fun H _ => by + classical + have hcard := card_subgroup_dvd_card H + rw [h, dvd_prime (Fact.out (p := p.Prime))] at hcard + refine' hcard.imp (fun h1 => _) fun hp => _ + · haveI := Fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1) + apply eq_bot_of_subsingleton + · exact eq_top_of_card_eq _ (hp.trans h.symm)⟩ #align is_simple_group_of_prime_card isSimpleGroup_of_prime_card #align is_simple_add_group_of_prime_card isSimpleAddGroup_of_prime_card @@ -462,11 +457,10 @@ open Subgroup variable {G : Type _} {H : Type _} [Group G] [Group H] /-- A group is commutative if the quotient by the center is cyclic. - Also see `commGroup_of_cycle_center_quotient` for the `comm_group` instance. -/ + Also see `commGroup_of_cycle_center_quotient` for the `CommGroup` instance. -/ @[to_additive commutative_of_add_cyclic_center_quotient - "A group is commutative if the quotient by\n - the center is cyclic. Also see `addCommGroup_of_cycle_center_quotient`\n - for the `add_comm_group` instance."] + "A group is commutative if the quotient by the center is cyclic. + Also see `addCommGroup_of_cycle_center_quotient` for the `AddCommGroup` instance."] theorem commutative_of_cyclic_center_quotient [IsCyclic H] (f : G →* H) (hf : f.ker ≤ center G) (a b : G) : a * b = b * a := let ⟨⟨x, y, (hxy : f y = x)⟩, (hx : ∀ a : f.range, a ∈ zpowers _)⟩ := @@ -476,8 +470,7 @@ theorem commutative_of_cyclic_center_quotient [IsCyclic H] (f : G →* H) (hf : have hm : x ^ m = f a := by simpa [Subtype.ext_iff] using hm have hn : x ^ n = f b := by simpa [Subtype.ext_iff] using hn have ha : y ^ (-m) * a ∈ center G := - hf (by - rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_self]) + hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_self]) have hb : y ^ (-n) * b ∈ center G := hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_self]) calc @@ -491,7 +484,7 @@ theorem commutative_of_cyclic_center_quotient [IsCyclic H] (f : G →* H) (hf : /-- A group is commutative if the quotient by the center is cyclic. -/ @[to_additive commutativeOfAddCycleCenterQuotient - "A group is commutative if the quotient by\n the center is cyclic."] + "A group is commutative if the quotient by the center is cyclic."] def commGroupOfCycleCenterQuotient [IsCyclic H] (f : G →* H) (hf : f.ker ≤ center G) : CommGroup G := { show Group G by infer_instance with mul_comm := commutative_of_cyclic_center_quotient f hf } @@ -519,6 +512,8 @@ instance (priority := 100) isCyclic : IsCyclic α := by apply Subgroup.mem_zpowers · rw [ht] apply Subgroup.mem_top +#align is_simple_group.is_cyclic IsSimpleGroup.isCyclic +#align is_simple_add_group.is_add_cyclic IsSimpleAddGroup.isAddCyclic @[to_additive] theorem prime_card [Fintype α] : (Fintype.card α).Prime := by @@ -549,7 +544,7 @@ end CommGroup end IsSimpleGroup -@[to_additive AddCommGroup.is_simple_iff_is_add_cyclic_and_prime_card] +@[to_additive AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card] theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Fintype α] [CommGroup α] : IsSimpleGroup α ↔ IsCyclic α ∧ (Fintype.card α).Prime := by constructor @@ -559,7 +554,7 @@ theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Fintype α] [CommGroup haveI : Fact (Fintype.card α).Prime := ⟨hp⟩ exact isSimpleGroup_of_prime_card rfl #align comm_group.is_simple_iff_is_cyclic_and_prime_card CommGroup.is_simple_iff_isCyclic_and_prime_card -#align add_comm_group.is_simple_iff_is_add_cyclic_and_prime_card AddCommGroup.is_simple_iff_is_add_cyclic_and_prime_card +#align add_comm_group.is_simple_iff_is_add_cyclic_and_prime_card AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card section Exponent @@ -601,4 +596,3 @@ theorem IsCyclic.exponent_eq_zero_of_infinite [Group α] [IsCyclic α] [Infinite #align is_add_cyclic.exponent_eq_zero_of_infinite IsAddCyclic.exponent_eq_zero_of_infinite end Exponent - diff --git a/Mathlib/LinearAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/Contraction.lean index edeea271f4840..af4018d73e7a4 100644 --- a/Mathlib/LinearAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/Contraction.lean @@ -126,7 +126,7 @@ theorem map_dualTensorHom (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q theorem comp_dualTensorHom (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) : dualTensorHom R N P (g ⊗ₜ[R] p) ∘ₗ dualTensorHom R M N (f ⊗ₜ[R] n) = g n • dualTensorHom R M P (f ⊗ₜ p) := by - ext m; + ext m simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smul, RingHom.id_apply, LinearMap.smul_apply] rw [smul_comm] @@ -333,4 +333,3 @@ theorem homTensorHomEquiv_apply (x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) : end CommRing end HomTensorHom - diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean index 91c2490c8bbae..b3049bf4340d0 100644 --- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean @@ -15,7 +15,7 @@ import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup /-! # The General Linear group $GL(n, R)$ -This file defines the elements of the General Linear group `general_linear_group n R`, +This file defines the elements of the General Linear group `Matrix.GeneralLinearGroup n R`, consisting of all invertible `n` by `n` `R`-matrices. ## Main definitions @@ -59,7 +59,7 @@ section CoeFnInstance -- Porting note: this instance was not the simp-normal form in mathlib3 but it is fine in mathlib4 -- because coercions get unfolded. /-- This instance is here for convenience, but is not the simp-normal form. -/ -instance : CoeFun (GL n R) fun _ => n → n → R where +instance instCoeFun : CoeFun (GL n R) fun _ => n → n → R where coe A := (A : Matrix n n R) end CoeFnInstance @@ -76,7 +76,7 @@ def det : GL n R →* Rˣ where map_mul' A B := Units.ext <| det_mul _ _ #align matrix.general_linear_group.det Matrix.GeneralLinearGroup.det -/-- The `GL n R` and `general_linear_group R n` groups are multiplicatively equivalent-/ +/-- The `GL n R` and `Matrix.GeneralLinearGroup R n` groups are multiplicatively equivalent-/ def toLin : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R) := Units.mapEquiv toLinAlgEquiv'.toMulEquiv #align matrix.general_linear_group.to_lin Matrix.GeneralLinearGroup.toLin @@ -247,7 +247,7 @@ namespace SpecialLinearGroup variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] -/-- `special_linear_group n R` embeds into `GL_pos n R` -/ +/-- `Matrix.SpecialLinearGroup n R` embeds into `GL_pos n R` -/ def toGLPos : SpecialLinearGroup n R →* GLPos n R where toFun A := ⟨(A : GL n R), show 0 < (↑A : Matrix n n R).det from A.prop.symm ▸ zero_lt_one⟩ map_one' := Subtype.ext <| Units.ext <| rfl @@ -270,8 +270,8 @@ theorem toGLPos_injective : Function.Injective (toGLPos : SpecialLinearGroup n R set_option linter.uppercaseLean3 false in #align matrix.special_linear_group.to_GL_pos_injective Matrix.SpecialLinearGroup.toGLPos_injective -/-- Coercing a `special_linear_group` via `GL_pos` and `GL` is the same as coercing striaght to a -matrix. -/ +/-- Coercing a `Matrix.SpecialLinearGroup` via `GL_pos` and `GL` is the same as coercing striaght to +a matrix. -/ @[simp] theorem coe_GLPos_coe_GL_coe_matrix (g : SpecialLinearGroup n R) : (↑(↑(↑g : GLPos n R) : GL n R) : Matrix n n R) = ↑g := diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index df0f9ebc66331..b15f343a04aa7 100644 --- a/Mathlib/RingTheory/IntegralDomain.lean +++ b/Mathlib/RingTheory/IntegralDomain.lean @@ -11,7 +11,6 @@ Authors: Johan Commelin, Chris Hughes import Mathlib.Data.Polynomial.RingDivision import Mathlib.GroupTheory.SpecificGroups.Cyclic import Mathlib.Algebra.GeomSum -import Mathlib.Tactic.LibrarySearch /-! # Integral domains @@ -20,8 +19,8 @@ Assorted theorems about integral domains. ## Main theorems -* `is_cyclic_of_subgroup_is_domain`: A finite subgroup of the units of an integral domain is cyclic. -* `fintype.field_of_domain`: A finite integral domain is a field. +* `isCyclic_of_subgroup_isDomain`: A finite subgroup of the units of an integral domain is cyclic. +* `Fintype.fieldOfDomain`: A finite integral domain is a field. ## TODO @@ -31,14 +30,10 @@ Prove Wedderburn's little theorem, which shows that all finite division rings ar integral domain, finite integral domain, finite field -/ -set_option autoImplicit false - section -open Finset Polynomial Function - -open BigOperators Nat +open Finset Polynomial Function BigOperators Nat section CancelMonoidWithZero @@ -57,8 +52,7 @@ theorem mul_left_bijective_of_finite₀ {a : M} (ha : a ≠ 0) : Bijective fun b def Fintype.groupWithZeroOfCancel (M : Type _) [CancelMonoidWithZero M] [DecidableEq M] [Fintype M] [Nontrivial M] : GroupWithZero M := { ‹Nontrivial M›, - ‹CancelMonoidWithZero - M› with + ‹CancelMonoidWithZero M› with inv := fun a => if h : a = 0 then 0 else Fintype.bijInv (mul_right_bijective_of_finite₀ h) 1 mul_inv_cancel := fun a ha => by simp [Inv.inv, dif_neg ha] @@ -154,7 +148,7 @@ theorem isCyclic_of_subgroup_isDomain [Finite G] (f : G →* R) (hf : Injective /-- The unit group of a finite integral domain is cyclic. To support `ℤˣ` and other infinite monoids with finite groups of units, this requires only -`finite Rˣ` rather than deducing it from `finite R`. -/ +`Finite Rˣ` rather than deducing it from `Finite R`. -/ instance [Finite Rˣ] : IsCyclic Rˣ := isCyclic_of_subgroup_isDomain (Units.coeHom R) <| Units.ext @@ -179,7 +173,7 @@ namespace Polynomial open Polynomial variable (K : Type) [Field K] [Algebra R[X] K] [IsFractionRing R[X] K] -set_option maxHeartbeats 0 + theorem div_eq_quo_add_rem_div (f : R[X]) {g : R[X]} (hg : g.Monic) : ∃ q r : R[X], r.degree < g.degree ∧ (algebraMap R[X] K f) / (algebraMap R[X] K g) = @@ -243,8 +237,7 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : (∑ g : G, f g) = let c := (univ.filter fun g => f.toHomUnits g = 1).card calc (∑ g : G, f g) = ∑ g : G, (f.toHomUnits g : R) := rfl - _ = - ∑ u : Rˣ in univ.image f.toHomUnits, + _ = ∑ u : Rˣ in univ.image f.toHomUnits, (univ.filter fun g => f.toHomUnits g = u).card • (u : R) := (sum_comp ((↑) : Rˣ → R) f.toHomUnits) _ = ∑ u : Rˣ in univ.image f.toHomUnits, c • (u : R) := @@ -257,7 +250,6 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : (∑ g : G, f g) = _ = c • (0 : R) := (congr_arg₂ _ rfl ?_) -- remaining goal 2, proven below _ = (0 : R) := smul_zero _ - · -- remaining goal 1 show (univ.filter fun g : G => f.toHomUnits g = u).card = c apply card_fiber_eq_of_mem_range f.toHomUnits diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index c4d91d7e079fd..cc46334405c2a 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -25,9 +25,7 @@ import Mathlib.RingTheory.Localization.FractionRing -/ -open HahnSeries - -open BigOperators Classical Polynomial +open HahnSeries BigOperators Classical Polynomial noncomputable section @@ -49,11 +47,11 @@ variable [Semiring R] instance : Coe (PowerSeries R) (LaurentSeries R) := ⟨HahnSeries.ofPowerSeries ℤ R⟩ -/-- Porting note: now a syntactic tautology and not needed elsewhere +/- Porting note: now a syntactic tautology and not needed elsewhere theorem coe_powerSeries (x : PowerSeries R) : (x : LaurentSeries R) = HahnSeries.ofPowerSeries ℤ R x := - rfl -#align laurent_series.coe_power_series LaurentSeries.coe_powerSeries -/ + rfl -/ +#noalign laurent_series.coe_power_series @[simp] theorem coeff_coe_powerSeries (x : PowerSeries R) (n : ℕ) : @@ -220,8 +218,8 @@ theorem coeff_coe (i : ℤ) : ((f : PowerSeries R) : LaurentSeries R).coeff i = if i < 0 then 0 else PowerSeries.coeff R i.natAbs f := by cases i - · rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, - if_neg (Int.coe_nat_nonneg _).not_lt, Int.natAbs_ofNat] + · rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.coe_nat_nonneg _).not_lt, + Int.natAbs_ofNat] · rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)] simp only [not_exists, RelEmbedding.coe_mk, Set.mem_image, not_and, Function.Embedding.coeFn_mk, Ne.def, toPowerSeries_symm_apply_coeff, mem_support, imp_true_iff, @@ -247,16 +245,9 @@ theorem coe_smul {S : Type _} [Semiring S] [Module R S] (r : R) (x : PowerSeries simp [coeff_coe, coeff_smul, smul_ite] #align power_series.coe_smul PowerSeries.coe_smul -/-- Porting note: RingHom.map_bit0 and RingHom.map_bit1 no longer exist -@[simp, norm_cast] -theorem coe_bit0 : ((bit0 f : PowerSeries R) : LaurentSeries R) = bit0 f := - (ofPowerSeries ℤ R).map_bit0 _ -#align power_series.coe_bit0 PowerSeries.coe_bit0 - -@[simp, norm_cast] -theorem coe_bit1 : ((bit1 f : PowerSeries R) : LaurentSeries R) = bit1 f := - (ofPowerSeries ℤ R).map_bit1 _ -#align power_series.coe_bit1 PowerSeries.coe_bit1 -/ +-- Porting note: RingHom.map_bit0 and RingHom.map_bit1 no longer exist +#noalign power_series.coe_bit0 +#noalign power_series.coe_bit1 @[simp, norm_cast] theorem coe_pow (n : ℕ) : ((f ^ n : PowerSeries R) : LaurentSeries R) = (ofPowerSeries ℤ R f) ^ n := diff --git a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean index a6272ef97f313..a0991e26d485e 100644 --- a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean +++ b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean @@ -29,9 +29,7 @@ variable {R : Type _} [CommRing R] (M : Submonoid R) {S : Type _} [CommRing S] variable [Algebra R S] {P : Type _} [CommRing P] -open Function - -open BigOperators +open Function BigOperators namespace IsLocalization @@ -45,7 +43,7 @@ variable [Algebra S T] [IsScalarTower R S T] -- This should only be defined when `S` is the localization `M⁻¹R`, hence the nolint. /-- Localizing wrt `M ⊆ R` and then wrt `N ⊆ S = M⁻¹R` is equal to the localization of `R` wrt this -module. See `localization_localization_is_localization`. +module. See `localization_localization_isLocalization`. -/ @[nolint unusedArguments] def localizationLocalizationSubmodule : Submonoid R := @@ -103,7 +101,6 @@ theorem localization_localization_eq_iff_exists [IsLocalization N T] (x y : R) : · rintro ⟨z, eq₁⟩ rcases IsLocalization.surj M (z : S) with ⟨⟨z', s⟩, eq₂⟩ dsimp only at eq₂ - let _a := (x * z' : R) suffices : (algebraMap R S) (x * z' : R) = (algebraMap R S) (y * z') · obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this refine ⟨⟨c * z', ?_⟩, ?_⟩ @@ -225,7 +222,7 @@ theorem isLocalization_of_submonoid_le (M N : Submonoid R) (h : M ≤ N) [IsLoca obtain ⟨⟨y₂, s₂⟩, e₂⟩ := IsLocalization.surj M x₂ refine' Iff.trans _ (Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).symm dsimp only at e₁ e₂⊢ - suffices : algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) ↔ + suffices : algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) ↔ ∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁)) · have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂) (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)