From 4c240da717b6abce32c521d202b0138c48c75c41 Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 16 Nov 2023 13:41:58 +0000 Subject: [PATCH] chore(RingTheory/{Algebraic, Localization/Integral}): rename decls to use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To | --- Mathlib/FieldTheory/AbelRuffini.lean | 6 +- Mathlib/FieldTheory/Adjoin.lean | 6 +- .../IsAlgClosed/AlgebraicClosure.lean | 6 +- Mathlib/FieldTheory/Minpoly/Field.lean | 2 +- Mathlib/FieldTheory/Normal.lean | 6 +- Mathlib/FieldTheory/Perfect.lean | 2 +- Mathlib/FieldTheory/PrimitiveElement.lean | 2 +- Mathlib/FieldTheory/Separable.lean | 2 +- .../SplittingField/IsSplittingField.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 2 +- .../NumberTheory/Cyclotomic/Discriminant.lean | 4 +- .../Cyclotomic/PrimitiveRoots.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/Rat.lean | 2 +- Mathlib/NumberTheory/NumberField/Norm.lean | 4 +- Mathlib/RingTheory/Adjoin/Field.lean | 2 +- Mathlib/RingTheory/Adjoin/PowerBasis.lean | 4 +- Mathlib/RingTheory/Algebraic.lean | 34 ++--- Mathlib/RingTheory/DedekindDomain/Ideal.lean | 2 +- .../DedekindDomain/IntegralClosure.lean | 6 +- Mathlib/RingTheory/Discriminant.lean | 6 +- Mathlib/RingTheory/FractionalIdeal.lean | 2 +- Mathlib/RingTheory/Ideal/Over.lean | 4 +- Mathlib/RingTheory/IntegralClosure.lean | 139 +++++++++--------- Mathlib/RingTheory/IntegrallyClosed.lean | 2 +- Mathlib/RingTheory/Jacobson.lean | 4 +- Mathlib/RingTheory/Localization/Integral.lean | 8 +- Mathlib/RingTheory/Norm.lean | 2 +- .../Polynomial/Eisenstein/IsIntegral.lean | 12 +- Mathlib/RingTheory/RingHom/Integral.lean | 2 +- Mathlib/RingTheory/Trace.lean | 2 +- 30 files changed, 140 insertions(+), 139 deletions(-) diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index 1ff1fdc3548265..6f9a8a2d764d14 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/Mathlib/FieldTheory/AbelRuffini.lean @@ -286,9 +286,9 @@ theorem isIntegral (α : solvableByRad F E) : IsIntegral F α := by revert α apply solvableByRad.induction · exact fun _ => isIntegral_algebraMap - · exact fun _ _ => isIntegral_add - · exact fun _ => isIntegral_neg - · exact fun _ _ => isIntegral_mul + · exact fun _ _ => IsIntegral.add + · exact fun _ => IsIntegral.neg + · exact fun _ _ => IsIntegral.mul · intro α hα exact Subalgebra.inv_mem_of_algebraic (integralClosure F (solvableByRad F E)) (show IsAlgebraic F ↑(⟨α, hα⟩ : integralClosure F (solvableByRad F E)) from diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index 5ca7f6fba692e1..473da0bbfb812c 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -1013,14 +1013,14 @@ theorem adjoin_minpoly_coeff_of_exists_primitive_element · exact subset_adjoin F _ (mem_frange_iff.mpr ⟨n, hn, rfl⟩) · exact not_mem_support_iff.mp hn ▸ zero_mem K' obtain ⟨p, hp⟩ := g.lifts_and_natDegree_eq_and_monic - g_lifts ((minpoly.monic <| isIntegral_of_finite K α).map _) + g_lifts ((minpoly.monic <| IsIntegral.of_finite K α).map _) have dvd_p : minpoly K' α ∣ p · apply minpoly.dvd rw [aeval_def, eval₂_eq_eval_map, hp.1, ← eval₂_eq_eval_map, ← aeval_def] exact minpoly.aeval K α have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) · intro K - have := adjoin.finrank (isIntegral_of_finite K α) + have := adjoin.finrank (IsIntegral.of_finite K α) erw [adjoin_eq_top_of_adjoin_eq_top F hprim, finrank_top K E] at this exact this refine eq_of_le_of_finrank_le' hsub ?_ @@ -1030,7 +1030,7 @@ theorem adjoin_minpoly_coeff_of_exists_primitive_element theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ finrank K L := - le_of_eq_of_le (IntermediateField.adjoin.finrank (isIntegral_of_finite _ _)).symm + le_of_eq_of_le (IntermediateField.adjoin.finrank (IsIntegral.of_finite _ _)).symm K⟮x⟯.toSubmodule.finrank_le #align minpoly.nat_degree_le minpoly.natDegree_le diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index e78cfb4934d3c2..63b811030098fb 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -140,9 +140,9 @@ theorem AdjoinMonic.isIntegral (z : AdjoinMonic k) : IsIntegral k z := by rw [← hp] induction p using MvPolynomial.induction_on generalizing z with | h_C => exact isIntegral_algebraMap - | h_add _ _ ha hb => exact isIntegral_add (ha _ rfl) (hb _ rfl) + | h_add _ _ ha hb => exact IsIntegral.add (ha _ rfl) (hb _ rfl) | h_X p f ih => - · refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_ + · refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_ refine ⟨f, f.2.1, ?_⟩ erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem] exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩) @@ -383,7 +383,7 @@ def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosureAux k := theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosureAux k) := fun z => isAlgebraic_iff_isIntegral.2 <| let ⟨n, x, hx⟩ := exists_ofStep k z - hx ▸ map_isIntegral (ofStepHom k n) (Step.isIntegral k n x) + hx ▸ IsIntegral.map (ofStepHom k n) (Step.isIntegral k n x) @[local instance] theorem isAlgClosure : IsAlgClosure k (AlgebraicClosureAux k) := ⟨AlgebraicClosureAux.instIsAlgClosed k, isAlgebraic k⟩ diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean index e17ca30fd570ff..637d352c5d7654 100644 --- a/Mathlib/FieldTheory/Minpoly/Field.lean +++ b/Mathlib/FieldTheory/Minpoly/Field.lean @@ -43,7 +43,7 @@ theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x #align minpoly.degree_le_of_ne_zero minpoly.degree_le_of_ne_zero theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 := - minpoly.ne_zero <| isIntegral_of_finite _ _ + minpoly.ne_zero <| IsIntegral.of_finite _ _ #align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property: diff --git a/Mathlib/FieldTheory/Normal.lean b/Mathlib/FieldTheory/Normal.lean index 315d7c46c65e57..c3490395fb6d29 100644 --- a/Mathlib/FieldTheory/Normal.lean +++ b/Mathlib/FieldTheory/Normal.lean @@ -114,7 +114,7 @@ theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' : rw [normal_iff] at h ⊢ intro x; specialize h (f.symm x) rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap] - exact ⟨map_isIntegral f h.1, splits_comp_of_splits _ _ h.2⟩ + exact ⟨IsIntegral.map f h.1, splits_comp_of_splits _ _ h.2⟩ #align normal.of_alg_equiv Normal.of_algEquiv theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E' := @@ -131,7 +131,7 @@ theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm)) refine normal_iff.mpr fun x ↦ ?_ haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p - have hx := isIntegral_of_finite F x + have hx := IsIntegral.of_finite F x let L := (p * minpoly F x).SplittingField have hL := splits_of_splits_mul' _ ?_ (SplittingField.splits (p * minpoly F x)) · let j : E →ₐ[F] L := IsSplittingField.lift E p hL.1 @@ -218,7 +218,7 @@ def AlgHom.restrictNormalAux [h : Normal F E] : (minpoly.dvd E _ (by simp [aeval_algHom_apply])) simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom] suffices IsIntegral F _ by exact isIntegral_of_isScalarTower this - exact map_isIntegral ϕ (map_isIntegral (toAlgHom F E K₁) (h.isIntegral z))⟩ + exact IsIntegral.map ϕ (IsIntegral.map (toAlgHom F E K₁) (h.isIntegral z))⟩ map_zero' := Subtype.ext ϕ.map_zero map_one' := Subtype.ext ϕ.map_one map_add' x y := Subtype.ext (ϕ.map_add x y) diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean index 061014f9ec6181..c2779d4e84f479 100644 --- a/Mathlib/FieldTheory/Perfect.lean +++ b/Mathlib/FieldTheory/Perfect.lean @@ -167,7 +167,7 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K have hg_dvd : g.map ι ∣ (X - C a) ^ p := by convert Polynomial.map_dvd ι (minpoly.dvd K a hfa) rw [sub_pow_char, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, ← ha_pow, map_pow] - have ha : IsIntegral K a := isIntegral_of_finite K a + have ha : IsIntegral K a := IsIntegral.of_finite K a have hg_pow : g.map ι = (X - C a) ^ (g.map ι).natDegree := by obtain ⟨q, -, hq⟩ := (dvd_prime_pow (prime_X_sub_C a) p).mp hg_dvd rw [eq_of_monic_of_associated ((minpoly.monic ha).map ι) ((monic_X_sub_C a).pow q) hq, diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index 062844ba9c2744..0a81327e537885 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/Mathlib/FieldTheory/PrimitiveElement.lean @@ -324,7 +324,7 @@ theorem finite_intermediateField_of_exists_primitive_element (halg : Algebra.IsA -- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α` over `K` -- which is a monic factor of `f` let g : IntermediateField F E → G := fun K ↦ - ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| isIntegral_of_finite K α).map _, by + ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| IsIntegral.of_finite K α).map _, by convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α) rw [Polynomial.map_map]; rfl⟩ -- The map `K ↦ g` is injective diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index 5e1349b5f2b79d..7c2354c789a395 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -544,7 +544,7 @@ theorem isSeparable_tower_top_of_isSeparable [IsSeparable F E] : IsSeparable K E theorem isSeparable_tower_bot_of_isSeparable [h : IsSeparable F E] : IsSeparable F K := isSeparable_iff.2 fun x => by refine' - (isSeparable_iff.1 h (algebraMap K E x)).imp isIntegral_tower_bot_of_isIntegral_field + (isSeparable_iff.1 h (algebraMap K E x)).imp IsIntegral.tower_bot_of_field fun hs => _ obtain ⟨q, hq⟩ := minpoly.dvd F x diff --git a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean b/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean index d1b373571a7cac..dbc2fa8888e06c 100644 --- a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean +++ b/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean @@ -129,7 +129,7 @@ def lift [Algebra K F] (f : K[X]) [IsSplittingField K L f] theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L := ⟨@Algebra.top_toSubmodule K L _ _ _ ▸ - adjoin_rootSet L f ▸ FG_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦ + adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦ if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy else isAlgebraic_iff_isIntegral.1 ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩ #align polynomial.is_splitting_field.finite_dimensional Polynomial.IsSplittingField.finiteDimensional diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index ecf9c5e101f148..8a217f0bc3fef4 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -309,7 +309,7 @@ theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] : Module.Finite A B := by classical rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2] - refine' FG_adjoin_of_finite _ fun b hb => _ + refine' fg_adjoin_of_finite _ fun b hb => _ · simp only [mem_singleton_iff, exists_eq_left] have : {b : B | b ^ (n : ℕ) = 1} = (nthRoots n (1 : B)).toFinset := Set.ext fun x => ⟨fun h => by simpa using h, fun h => by simpa using h⟩ diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index 83c3817c8cbafe..57dcb6facf33c4 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -46,9 +46,9 @@ theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) : fun i j => toMatrix_isIntegral H₂ _ _ _ _ · exact hζ.isIntegral n.pos · refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral n.pos) - · exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one + · exact IsIntegral.sub (hζ.isIntegral n.pos) isIntegral_one · refine' minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) _ - exact isIntegral_sub (hζ.isIntegral n.pos) isIntegral_one + exact IsIntegral.sub (hζ.isIntegral n.pos) isIntegral_one #align is_primitive_root.discr_zeta_eq_discr_zeta_sub_one IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one end IsPrimitiveRoot diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 6e64e5c3096e63..a97b0a42257344 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -137,7 +137,7 @@ theorem powerBasis_gen_mem_adjoin_zeta_sub_one : @[simps!] noncomputable def subOnePowerBasis : PowerBasis K L := (hζ.powerBasis K).ofGenMemAdjoin - (isIntegral_sub (IsCyclotomicExtension.integral {n} K L ζ) isIntegral_one) + (IsIntegral.sub (IsCyclotomicExtension.integral {n} K L ζ) isIntegral_one) (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _) #align is_primitive_root.sub_one_power_basis IsPrimitiveRoot.subOnePowerBasis diff --git a/Mathlib/NumberTheory/Cyclotomic/Rat.lean b/Mathlib/NumberTheory/Cyclotomic/Rat.lean index ff9183d9b9fb24..51464c8a80fd16 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Rat.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Rat.lean @@ -82,7 +82,7 @@ theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExt (le_integralClosure_iff_isIntegral.1 (adjoin_le_integralClosure (hζ.isIntegral (p ^ k).pos)) _) let B := hζ.subOnePowerBasis ℚ - have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.isIntegral (p ^ k).pos) isIntegral_one + have hint : IsIntegral ℤ B.gen := IsIntegral.sub (hζ.isIntegral (p ^ k).pos) isIntegral_one -- Porting note: the following `haveI` was not needed because the locale `cyclotomic` set it -- as instances. letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean index 0e909ba5fb6b12..ffd36b21e8bba2 100644 --- a/Mathlib/NumberTheory/NumberField/Norm.lean +++ b/Mathlib/NumberTheory/NumberField/Norm.lean @@ -58,7 +58,7 @@ theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L) refine' @isUnit_of_mul_isUnit_right (𝓞 L) _ ⟨(univ \ {AlgEquiv.refl}).prod fun σ : L ≃ₐ[K] L => σ x, - prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩ _ _ + prod_mem fun σ _ => IsIntegral.map (σ : L →+* L).toIntAlgHom x.2⟩ _ _ convert hx using 1 ext push_cast @@ -74,7 +74,7 @@ theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L classical have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L := Subalgebra.prod_mem _ fun σ _ => - (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x)) + (mem_ringOfIntegers _ _).2 (IsIntegral.map σ (RingOfIntegers.isIntegral_coe x)) refine' ⟨⟨_, hint⟩, Subtype.ext _⟩ rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms] simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)] diff --git a/Mathlib/RingTheory/Adjoin/Field.lean b/Mathlib/RingTheory/Adjoin/Field.lean index 1f829408485a2c..b9c697660e63ae 100644 --- a/Mathlib/RingTheory/Adjoin/Field.lean +++ b/Mathlib/RingTheory/Adjoin/Field.lean @@ -67,7 +67,7 @@ theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L] rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin] set Ks := Algebra.adjoin F (s : Set K) haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1 - (FG_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule + (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule letI := fieldOfFiniteDimensional F Ks letI := (f : Ks →+* L).toAlgebra have H5 : IsIntegral Ks a := isIntegral_of_isScalarTower H1 diff --git a/Mathlib/RingTheory/Adjoin/PowerBasis.lean b/Mathlib/RingTheory/Adjoin/PowerBasis.lean index 707622842f01d1..6b31924671fc89 100644 --- a/Mathlib/RingTheory/Adjoin/PowerBasis.lean +++ b/Mathlib/RingTheory/Adjoin/PowerBasis.lean @@ -138,7 +138,7 @@ theorem repr_mul_isIntegral [IsDomain S] {x y : A} (hx : ∀ i, IsIntegral R (B. refine' IsIntegral.sum _ fun I _ => _ simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finsupp.coe_smul, Pi.smul_apply, id.smul_eq_mul] - refine' isIntegral_mul (hy _) (isIntegral_mul (hx _) _) + refine' IsIntegral.mul (hy _) (IsIntegral.mul (hx _) _) simp only [coe_basis, ← pow_add] refine' repr_gen_pow_isIntegral hB hmin _ _ #align power_basis.repr_mul_is_integral PowerBasis.repr_mul_isIntegral @@ -181,7 +181,7 @@ theorem toMatrix_isIntegral {B B' : PowerBasis K S} {P : R[X]} (h : aeval B.gen refine' IsIntegral.sum _ fun n _ => _ rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, LinearEquiv.map_smul, algebraMap_smul] - exact isIntegral_smul _ (repr_gen_pow_isIntegral hB hmin _ _) + exact IsIntegral.smul _ (repr_gen_pow_isIntegral hB hmin _ _) #align power_basis.to_matrix_is_integral PowerBasis.toMatrix_isIntegral end PowerBasis diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean index 9ac73593f16a51..ce9bed606eda97 100644 --- a/Mathlib/RingTheory/Algebraic.lean +++ b/Mathlib/RingTheory/Algebraic.lean @@ -136,23 +136,23 @@ theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [Field R] [Field A] open IsScalarTower -theorem isAlgebraic_algebraMap_of_isAlgebraic {a : S} : +protected theorem IsAlgebraic.algebraMap {a : S} : IsAlgebraic R a → IsAlgebraic R (algebraMap S A a) := fun ⟨f, hf₁, hf₂⟩ => ⟨f, hf₁, by rw [aeval_algebraMap_apply, hf₂, map_zero]⟩ -#align is_algebraic_algebra_map_of_is_algebraic isAlgebraic_algebraMap_of_isAlgebraic +#align is_algebraic_algebra_map_of_is_algebraic IsAlgebraic.algebraMap /-- This is slightly more general than `isAlgebraic_algebraMap_of_isAlgebraic` in that it allows noncommutative intermediate rings `A`. -/ -theorem isAlgebraic_algHom_of_isAlgebraic {B} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A} +protected theorem IsAlgebraic.algHom {B} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A} (h : IsAlgebraic R a) : IsAlgebraic R (f a) := let ⟨p, hp, ha⟩ := h ⟨p, hp, by rw [aeval_algHom, f.comp_apply, ha, map_zero]⟩ -#align is_algebraic_alg_hom_of_is_algebraic isAlgebraic_algHom_of_isAlgebraic +#align is_algebraic_alg_hom_of_is_algebraic IsAlgebraic.algHom /-- Transfer `Algebra.IsAlgebraic` across an `AlgEquiv`. -/ theorem AlgEquiv.isAlgebraic {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) (h : Algebra.IsAlgebraic R A) : Algebra.IsAlgebraic R B := fun b => by - convert← isAlgebraic_algHom_of_isAlgebraic e.toAlgHom (h _); refine e.apply_symm_apply ?_ + convert← IsAlgebraic.algHom e.toAlgHom (h _); refine e.apply_symm_apply ?_ #align alg_equiv.is_algebraic AlgEquiv.isAlgebraic theorem AlgEquiv.isAlgebraic_iff {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) : @@ -163,19 +163,19 @@ theorem AlgEquiv.isAlgebraic_iff {B} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) theorem isAlgebraic_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) : IsAlgebraic R (algebraMap S A a) ↔ IsAlgebraic R a := ⟨fun ⟨p, hp0, hp⟩ => ⟨p, hp0, h (by rwa [map_zero, ← aeval_algebraMap_apply])⟩, - isAlgebraic_algebraMap_of_isAlgebraic⟩ + IsAlgebraic.algebraMap⟩ #align is_algebraic_algebra_map_iff isAlgebraic_algebraMap_iff -theorem isAlgebraic_of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) : +theorem IsAlgebraic.of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) : IsAlgebraic R r := by obtain ⟨p, p_nonzero, hp⟩ := ht refine ⟨Polynomial.expand _ n p, ?_, ?_⟩ · rwa [Polynomial.expand_ne_zero hn] · rwa [Polynomial.expand_aeval n p r] -#align is_algebraic_of_pow isAlgebraic_of_pow +#align is_algebraic_of_pow IsAlgebraic.of_pow theorem Transcendental.pow {r : A} (ht : Transcendental R r) {n : ℕ} (hn : 0 < n) : - Transcendental R (r ^ n) := fun ht' => ht <| isAlgebraic_of_pow hn ht' + Transcendental R (r ^ n) := fun ht' => ht <| IsAlgebraic.of_pow hn ht' #align transcendental.pow Transcendental.pow end zero_ne_one @@ -213,19 +213,19 @@ variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] /-- If x is algebraic over R, then x is algebraic over S when S is an extension of R, and the map from `R` to `S` is injective. -/ -theorem isAlgebraic_of_larger_base_of_injective +theorem IsAlgebraic.of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S)) {x : A} (A_alg : IsAlgebraic R x) : IsAlgebraic S x := let ⟨p, hp₁, hp₂⟩ := A_alg ⟨p.map (algebraMap _ _), by rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩ -#align is_algebraic_of_larger_base_of_injective isAlgebraic_of_larger_base_of_injective +#align is_algebraic_of_larger_base_of_injective IsAlgebraic.of_larger_base_of_injective /-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R, and the map from `R` to `S` is injective. -/ theorem Algebra.isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S)) (A_alg : IsAlgebraic R A) : IsAlgebraic S A := fun x => - _root_.isAlgebraic_of_larger_base_of_injective hinj (A_alg x) + IsAlgebraic.of_larger_base_of_injective hinj (A_alg x) #align algebra.is_algebraic_of_larger_base_of_injective Algebra.isAlgebraic_of_larger_base_of_injective end CommRing @@ -239,10 +239,10 @@ variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] variable (L) /-- If x is algebraic over K, then x is algebraic over L when L is an extension of K -/ -theorem isAlgebraic_of_larger_base {x : A} (A_alg : IsAlgebraic K x) : +theorem IsAlgebraic.of_larger_base {x : A} (A_alg : IsAlgebraic K x) : IsAlgebraic L x := - isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg -#align is_algebraic_of_larger_base isAlgebraic_of_larger_base + IsAlgebraic.of_larger_base_of_injective (algebraMap K L).injective A_alg +#align is_algebraic_of_larger_base IsAlgebraic.of_larger_base /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/ theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A := @@ -251,8 +251,8 @@ theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebra variable (K) -theorem isAlgebraic_of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e := - isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K e) +theorem IsAlgebraic.of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e := + isAlgebraic_iff_isIntegral.mpr (IsIntegral.of_finite K e) variable (A) diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index 6c7d0f1cf3af33..27aae3ac721dae 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -497,7 +497,7 @@ theorem coe_ideal_mul_inv [h : IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ ← mem_one_iff] at this -- For that, we'll find a subalgebra that is f.g. as a module and contains `x`. -- `A` is a noetherian ring, so we just need to find a subalgebra between `{x}` and `I⁻¹`. - rw [mem_integralClosure_iff_mem_FG] + rw [mem_integralClosure_iff_mem_fg] have x_mul_mem : ∀ b ∈ (I⁻¹ : FractionalIdeal A⁰ K), x * b ∈ (I⁻¹ : FractionalIdeal A⁰ K) := by intro b hb rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI0)] diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 9205dbe5c8a308..943aa970b6dc11 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -111,7 +111,7 @@ theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type*} rw [← IsScalarTower.algebraMap_smul K (Classical.choose (hc' i)) (db i)] refine' ⟨fun i => db.repr (algebraMap C L x) i, fun i => _, (db.sum_repr _).symm⟩ simp_rw [BilinForm.dualBasis_repr_apply] - exact isIntegral_trace (isIntegral_mul hx (hb_int i)) + exact isIntegral_trace (IsIntegral.mul hx (hb_int i)) #align is_integral_closure.range_le_span_dual_basis IsIntegralClosure.range_le_span_dualBasis theorem integralClosure_le_span_dualBasis [IsSeparable K L] {ι : Type*} [Fintype ι] [DecidableEq ι] @@ -141,9 +141,9 @@ theorem exists_integral_multiples (s : Finset L) : refine' ⟨y * y', mul_ne_zero hy hy', fun x'' hx'' => _⟩ rcases Finset.mem_insert.mp hx'' with (rfl | hx'') · rw [mul_smul, Algebra.smul_def, Algebra.smul_def, mul_comm _ x'', hx'] - exact isIntegral_mul isIntegral_algebraMap x'.2 + exact IsIntegral.mul isIntegral_algebraMap x'.2 · rw [mul_comm, mul_smul, Algebra.smul_def] - exact isIntegral_mul isIntegral_algebraMap (hs _ hx'') + exact IsIntegral.mul isIntegral_algebraMap (hs _ hx'') · rw [IsScalarTower.algebraMap_eq A K L] apply (algebraMap K L).injective.comp exact IsFractionRing.injective _ _ diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 5ba6c01f0ecc1a..65b1ab723b9e08 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -290,7 +290,7 @@ variable {R : Type z} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R theorem discr_isIntegral {b : ι → L} (h : ∀ i, IsIntegral R (b i)) : IsIntegral R (discr K b) := by classical rw [discr_def] - exact IsIntegral.det fun i j => isIntegral_trace (isIntegral_mul (h i) (h j)) + exact IsIntegral.det fun i j => isIntegral_trace (IsIntegral.mul (h i) (h j)) #align algebra.discr_is_integral Algebra.discr_isIntegral /-- If `b` and `b'` are `ℚ`-bases of a number field `K` such that @@ -364,12 +364,12 @@ theorem discr_mul_isIntegral_mem_adjoin [IsSeparable K L] [IsIntegrallyClosed R] exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| - isIntegral_trace <| isIntegral_mul hz <| IsIntegral.pow hint _) + isIntegral_trace <| IsIntegral.mul hz <| IsIntegral.pow hint _) · simp only [updateColumn_apply, hji, PowerBasis.coe_basis] exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| - isIntegral_trace <| isIntegral_mul (IsIntegral.pow hint _) (IsIntegral.pow hint _)) + isIntegral_trace <| IsIntegral.mul (IsIntegral.pow hint _) (IsIntegral.pow hint _)) #align algebra.discr_mul_is_integral_mem_adjoin Algebra.discr_mul_isIntegral_mem_adjoin end Integral diff --git a/Mathlib/RingTheory/FractionalIdeal.lean b/Mathlib/RingTheory/FractionalIdeal.lean index 21a9b567ba34b1..df6bbb4c072c75 100644 --- a/Mathlib/RingTheory/FractionalIdeal.lean +++ b/Mathlib/RingTheory/FractionalIdeal.lean @@ -1598,7 +1598,7 @@ variable (x : P) (hx : IsIntegral R x) /-- `A[x]` is a fractional ideal for every integral `x`. -/ theorem isFractional_adjoin_integral : IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R ({x} : Set P))) := - isFractional_of_fg (FG_adjoin_singleton_of_integral x hx) + isFractional_of_fg (IsIntegral.fg_adjoin_singleton x hx) #align fractional_ideal.is_fractional_adjoin_integral FractionalIdeal.isFractional_adjoin_integral /-- `FractionalIdeal.adjoinIntegral (S : Submonoid R) x hx` is `R[x]` as a fractional ideal, diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index ea48a9a5c34c90..adb99cb982ce66 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/Mathlib/RingTheory/Ideal/Over.lean @@ -285,7 +285,7 @@ theorem isMaximal_comap_of_isIntegral_of_isMaximal (hRS : Algebra.IsIntegral R S refine' Ideal.Quotient.maximal_of_isField _ _ haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _ exact - isField_of_isIntegral_of_isField (isIntegral_quotient_of_isIntegral hRS) + isField_of_isIntegral_of_isField (Algebra.IsIntegral.quotient hRS) algebraMap_quotient_injective (by rwa [← Quotient.maximal_ideal_iff_isField_quotient]) #align ideal.is_maximal_comap_of_is_integral_of_is_maximal Ideal.isMaximal_comap_of_isIntegral_of_isMaximal @@ -387,7 +387,7 @@ theorem exists_ideal_over_prime_of_isIntegral (H : Algebra.IsIntegral R S) (P : ∃ Q ≥ I, IsPrime Q ∧ Q.comap (algebraMap R S) = P := by obtain ⟨Q' : Ideal (S ⧸ I), ⟨Q'_prime, hQ'⟩⟩ := @exists_ideal_over_prime_of_isIntegral' (R ⧸ I.comap (algebraMap R S)) _ (S ⧸ I) _ - Ideal.quotientAlgebra _ (isIntegral_quotient_of_isIntegral H) + Ideal.quotientAlgebra _ (Algebra.IsIntegral.quotient H) (map (Ideal.Quotient.mk (I.comap (algebraMap R S))) P) (map_isPrime_of_surjective Quotient.mk_surjective (by simp [hIP])) (le_trans (le_of_eq ((RingHom.injective_iff_ker_eq_bot _).1 algebraMap_quotient_injective)) diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index c09543aebeccfe..cd905f93485929 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -121,7 +121,7 @@ variable [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] variable (K) -theorem isIntegral_of_finite (e : A) : IsIntegral K e := +theorem IsIntegral.of_finite (e : A) : IsIntegral K e := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 inferInstance) _ variable (A) @@ -141,16 +141,16 @@ variable [CommRing R] [CommRing A] [CommRing B] [CommRing S] variable [Algebra R A] [Algebra R B] (f : R →+* S) -theorem map_isIntegral {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C] +theorem IsIntegral.map {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C] [IsScalarTower R A B] [Algebra A C] [IsScalarTower R A C] {b : B} [AlgHomClass F A B C] (f : F) (hb : IsIntegral R b) : IsIntegral R (f b) := by obtain ⟨P, hP⟩ := hb refine' ⟨P, hP.1, _⟩ rw [← aeval_def, show (aeval (f b)) P = (aeval (f b)) (P.map (algebraMap R A)) by simp, aeval_algHom_apply, aeval_map_algebraMap, aeval_def, hP.2, _root_.map_zero] -#align map_is_integral map_isIntegral +#align map_is_integral IsIntegral.map -theorem isIntegral_map_of_comp_eq_of_isIntegral {R S T U : Type*} [CommRing R] [CommRing S] +theorem IsIntegral.map_of_comp_eq {R S T U : Type*} [CommRing R] [CommRing S] [CommRing T] [CommRing U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U) (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) {a : S} (ha : IsIntegral R a) : IsIntegral T (ψ a) := by @@ -159,11 +159,11 @@ theorem isIntegral_map_of_comp_eq_of_isIntegral {R S T U : Type*} [CommRing R] [ refine' ⟨p.map φ, hp.left.map _, _⟩ rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.right, RingHom.map_zero] -#align is_integral_map_of_comp_eq_of_is_integral isIntegral_map_of_comp_eq_of_isIntegral +#align is_integral_map_of_comp_eq_of_is_integral IsIntegral.map_of_comp_eq theorem isIntegral_algHom_iff {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x := by - refine' ⟨_, map_isIntegral f⟩ + refine' ⟨_, IsIntegral.map f⟩ rintro ⟨p, hp, hx⟩ use p, hp rwa [← f.comp_algebraMap, ← AlgHom.coe_toRingHom, ← Polynomial.hom_eval₂, AlgHom.coe_toRingHom, @@ -173,7 +173,7 @@ theorem isIntegral_algHom_iff {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Alg @[simp] theorem isIntegral_algEquiv {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x := - ⟨fun h => by simpa using map_isIntegral f.symm.toAlgHom h, map_isIntegral f.toAlgHom⟩ + ⟨fun h => by simpa using IsIntegral.map f.symm.toAlgHom h, IsIntegral.map f.toAlgHom⟩ #align is_integral_alg_equiv isIntegral_algEquiv theorem isIntegral_of_isScalarTower [Algebra A B] [IsScalarTower R A B] {x : B} @@ -184,14 +184,15 @@ theorem isIntegral_of_isScalarTower [Algebra A B] [IsScalarTower R A B] {x : B} theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B} [RingHomClass F B C] (f : F) (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) := - map_isIntegral (f : B →+* C).toIntAlgHom hb + IsIntegral.map (f : B →+* C).toIntAlgHom hb #align map_is_integral_int map_isIntegral_int -theorem isIntegral_ofSubring {x : A} (T : Subring R) (hx : IsIntegral T x) : IsIntegral R x := +theorem IsIntegral.of_subring {x : A} (T : Subring R) (hx : IsIntegral T x) : IsIntegral R x := isIntegral_of_isScalarTower hx -#align is_integral_of_subring isIntegral_ofSubring +#align is_integral_of_subring IsIntegral.of_subring -theorem IsIntegral.algebraMap [Algebra A B] [IsScalarTower R A B] {x : A} (h : IsIntegral R x) : +protected theorem IsIntegral.algebraMap [Algebra A B] [IsScalarTower R A B] {x : A} + (h : IsIntegral R x) : IsIntegral R (algebraMap A B x) := by rcases h with ⟨f, hf, hx⟩ use f, hf @@ -211,10 +212,10 @@ theorem isIntegral_iff_isIntegral_closure_finite {r : A} : refine' ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, _⟩ rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr] rcases hr with ⟨s, _, hsr⟩ - exact isIntegral_ofSubring _ hsr + exact IsIntegral.of_subring _ hsr #align is_integral_iff_is_integral_closure_finite isIntegral_iff_isIntegral_closure_finite -theorem FG_adjoin_singleton_of_integral (x : A) (hx : IsIntegral R x) : +theorem IsIntegral.fg_adjoin_singleton (x : A) (hx : IsIntegral R x) : (Algebra.adjoin R ({x} : Set A)).toSubmodule.FG := by rcases hx with ⟨f, hfm, hfx⟩ exists Finset.image ((· ^ ·) x) (Finset.range (natDegree f + 1)) @@ -242,9 +243,9 @@ theorem FG_adjoin_singleton_of_integral (x : A) (hx : IsIntegral R x) : rw [degree_le_iff_coeff_zero] at this rw [mem_support_iff] at hkq; apply hkq; apply this exact lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 hk) -#align fg_adjoin_singleton_of_integral FG_adjoin_singleton_of_integral +#align fg_adjoin_singleton_of_integral IsIntegral.fg_adjoin_singleton -theorem FG_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) : +theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) : (Algebra.adjoin R s).toSubmodule.FG := Set.Finite.induction_on hfs (fun _ => @@ -255,18 +256,18 @@ theorem FG_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsI rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule] exact FG.mul (ih fun i hi => his i <| Set.mem_insert_of_mem a hi) - (FG_adjoin_singleton_of_integral _ <| his a <| Set.mem_insert a s)) + (IsIntegral.fg_adjoin_singleton _ <| his a <| Set.mem_insert a s)) his -#align fg_adjoin_of_finite FG_adjoin_of_finite +#align fg_adjoin_of_finite fg_adjoin_of_finite theorem isNoetherian_adjoin_finset [IsNoetherianRing R] (s : Finset A) (hs : ∀ x ∈ s, IsIntegral R x) : IsNoetherian R (Algebra.adjoin R (↑s : Set A)) := - isNoetherian_of_fg_of_noetherian _ (FG_adjoin_of_finite s.finite_toSet hs) + isNoetherian_of_fg_of_noetherian _ (fg_adjoin_of_finite s.finite_toSet hs) #align is_noetherian_adjoin_finset isNoetherian_adjoin_finset /-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module, then all elements of `S` are integral over `R`. -/ -theorem isIntegral_of_mem_of_FG (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x : A) (hx : x ∈ S) : +theorem IsIntegral.of_mem_of_fg (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x : A) (hx : x ∈ S) : IsIntegral R x := by -- say `x ∈ S`. We want to prove that `x` is integral over `R`. -- Say `S` is generated as an `R`-module by the set `y`. @@ -292,7 +293,7 @@ theorem isIntegral_of_mem_of_FG (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x let S₀ : Subring R := Subring.closure ↑(lx.frange ∪ Finset.biUnion Finset.univ (Finsupp.frange ∘ ly)) -- It suffices to prove that `x` is integral over `S₀`. - refine' isIntegral_ofSubring S₀ _ + refine' IsIntegral.of_subring S₀ _ letI : CommRing S₀ := SubringClass.toCommRing S₀ letI : Algebra S₀ A := Algebra.ofSubring S₀ -- Claim: the `S₀`-module span (in `A`) of the set `y ∪ {1}` is closed under @@ -365,7 +366,7 @@ theorem isIntegral_of_mem_of_FG (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x change (⟨_, this⟩ : S₀) • r ∈ _ rw [Finsupp.mem_supported] at hlx1 exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| hlx1 hr) _ -#align is_integral_of_mem_of_fg isIntegral_of_mem_of_FG +#align is_integral_of_mem_of_fg IsIntegral.of_mem_of_fg theorem Module.End.isIntegral {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] : Algebra.IsIntegral R (Module.End R M) := @@ -419,7 +420,7 @@ variable {f} theorem RingHom.Finite.to_isIntegral (h : f.Finite) : f.IsIntegral := letI := f.toAlgebra - fun _ => isIntegral_of_mem_of_FG ⊤ h.1 _ trivial + fun _ => IsIntegral.of_mem_of_fg ⊤ h.1 _ trivial #align ring_hom.finite.to_is_integral RingHom.Finite.to_isIntegral alias RingHom.IsIntegral.of_finite := RingHom.Finite.to_isIntegral @@ -431,7 +432,7 @@ theorem RingHom.IsIntegral.to_finite (h : f.IsIntegral) (h' : f.FiniteType) : f. constructor change (⊤ : Subalgebra R S).toSubmodule.FG rw [← hs] - exact FG_adjoin_of_finite (Set.toFinite _) fun x _ => h x + exact fg_adjoin_of_finite (Set.toFinite _) fun x _ => h x #align ring_hom.is_integral.to_finite RingHom.IsIntegral.to_finite alias RingHom.Finite.of_isIntegral_of_finiteType := RingHom.IsIntegral.to_finite @@ -459,7 +460,7 @@ theorem Algebra.IsIntegral.finite (h : Algebra.IsIntegral R A) [h' : Algebra.Fin #align algebra.is_integral.finite Algebra.IsIntegral.finite theorem Algebra.IsIntegral.of_finite [h : Module.Finite R A] : Algebra.IsIntegral R A := - fun _ ↦ isIntegral_of_mem_of_FG ⊤ h.1 _ trivial + fun _ ↦ IsIntegral.of_mem_of_fg ⊤ h.1 _ trivial #align algebra.is_integral.of_finite Algebra.IsIntegral.of_finite /-- finite = integral + finite type -/ @@ -473,17 +474,17 @@ variable (f) theorem RingHom.is_integral_of_mem_closure {x y z : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure ({x, y} : Set S)) : f.IsIntegralElem z := by letI : Algebra R S := f.toAlgebra - have := (FG_adjoin_singleton_of_integral x hx).mul (FG_adjoin_singleton_of_integral y hy) + have := (IsIntegral.fg_adjoin_singleton x hx).mul (IsIntegral.fg_adjoin_singleton y hy) rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this exact - isIntegral_of_mem_of_FG (Algebra.adjoin R {x, y}) this z + IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono (Set.subset_union_right _ _) hz) #align ring_hom.is_integral_of_mem_closure RingHom.is_integral_of_mem_closure -theorem isIntegral_of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) +theorem IsIntegral.of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z ∈ Subring.closure ({x, y} : Set A)) : IsIntegral R z := (algebraMap R A).is_integral_of_mem_closure hx hy hz -#align is_integral_of_mem_closure isIntegral_of_mem_closure +#align is_integral_of_mem_closure IsIntegral.of_mem_closure theorem RingHom.is_integral_zero : f.IsIntegralElem 0 := f.map_zero ▸ f.is_integral_map @@ -507,28 +508,28 @@ theorem RingHom.is_integral_add {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIn Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)) #align ring_hom.is_integral_add RingHom.is_integral_add -theorem isIntegral_add {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : +theorem IsIntegral.add {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x + y) := (algebraMap R A).is_integral_add hx hy -#align is_integral_add isIntegral_add +#align is_integral_add IsIntegral.add theorem RingHom.is_integral_neg {x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x) := f.is_integral_of_mem_closure hx hx (Subring.neg_mem _ (Subring.subset_closure (Or.inl rfl))) #align ring_hom.is_integral_neg RingHom.is_integral_neg -theorem isIntegral_neg {x : A} (hx : IsIntegral R x) : IsIntegral R (-x) := +theorem IsIntegral.neg {x : A} (hx : IsIntegral R x) : IsIntegral R (-x) := (algebraMap R A).is_integral_neg hx -#align is_integral_neg isIntegral_neg +#align is_integral_neg IsIntegral.neg theorem RingHom.is_integral_sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x - y) := by simpa only [sub_eq_add_neg] using f.is_integral_add hx (f.is_integral_neg hy) #align ring_hom.is_integral_sub RingHom.is_integral_sub -theorem isIntegral_sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : +theorem IsIntegral.sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x - y) := (algebraMap R A).is_integral_sub hx hy -#align is_integral_sub isIntegral_sub +#align is_integral_sub IsIntegral.sub theorem RingHom.is_integral_mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x * y) := @@ -536,24 +537,24 @@ theorem RingHom.is_integral_mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIn (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))) #align ring_hom.is_integral_mul RingHom.is_integral_mul -theorem isIntegral_mul {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : +theorem IsIntegral.mul {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x * y) := (algebraMap R A).is_integral_mul hx hy -#align is_integral_mul isIntegral_mul +#align is_integral_mul IsIntegral.mul -theorem isIntegral_smul [Algebra S A] [Algebra R S] [IsScalarTower R S A] {x : A} (r : R) +theorem IsIntegral.smul [Algebra S A] [Algebra R S] [IsScalarTower R S A] {x : A} (r : R) (hx : IsIntegral S x) : IsIntegral S (r • x) := by rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S A] - exact isIntegral_mul isIntegral_algebraMap hx -#align is_integral_smul isIntegral_smul + exact IsIntegral.mul isIntegral_algebraMap hx +#align is_integral_smul IsIntegral.smul -theorem isIntegral_of_pow {x : A} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : +theorem IsIntegral.of_pow {x : A} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : IsIntegral R x := by rcases hx with ⟨p, ⟨hmonic, heval⟩⟩ exact ⟨expand R n p, Monic.expand hn hmonic, by rwa [eval₂_eq_eval_map, map_expand, expand_eval, ← eval₂_eq_eval_map]⟩ -#align is_integral_of_pow isIntegral_of_pow +#align is_integral_of_pow IsIntegral.of_pow variable (R A) @@ -562,17 +563,17 @@ def integralClosure : Subalgebra R A where carrier := { r | IsIntegral R r } zero_mem' := isIntegral_zero one_mem' := isIntegral_one - add_mem' := isIntegral_add - mul_mem' := isIntegral_mul + add_mem' := IsIntegral.add + mul_mem' := IsIntegral.mul algebraMap_mem' _ := isIntegral_algebraMap #align integral_closure integralClosure -theorem mem_integralClosure_iff_mem_FG {r : A} : +theorem mem_integralClosure_iff_mem_fg {r : A} : r ∈ integralClosure R A ↔ ∃ M : Subalgebra R A, M.toSubmodule.FG ∧ r ∈ M := ⟨fun hr => - ⟨Algebra.adjoin R {r}, FG_adjoin_singleton_of_integral _ hr, Algebra.subset_adjoin rfl⟩, - fun ⟨M, Hf, hrM⟩ => isIntegral_of_mem_of_FG M Hf _ hrM⟩ -#align mem_integral_closure_iff_mem_fg mem_integralClosure_iff_mem_FG + ⟨Algebra.adjoin R {r}, IsIntegral.fg_adjoin_singleton _ hr, Algebra.subset_adjoin rfl⟩, + fun ⟨M, Hf, hrM⟩ => IsIntegral.of_mem_of_fg M Hf _ hrM⟩ +#align mem_integral_closure_iff_mem_fg mem_integralClosure_iff_mem_fg variable {R} {A} @@ -604,9 +605,9 @@ theorem integralClosure_map_algEquiv (f : A ≃ₐ[R] B) : rw [Subalgebra.mem_map] constructor · rintro ⟨x, hx, rfl⟩ - exact map_isIntegral f hx + exact IsIntegral.map f hx · intro hy - use f.symm y, map_isIntegral (f.symm : B →ₐ[R] A) hy + use f.symm y, IsIntegral.map (f.symm : B →ₐ[R] A) hy simp #align integral_closure_map_alg_equiv integralClosure_map_algEquiv @@ -625,16 +626,16 @@ theorem RingHom.isIntegral_of_isIntegral_mul_unit (x y : S) (r : R) (hr : f r * rw [mul_comm x y, ← mul_assoc, hr, one_mul] #align ring_hom.is_integral_of_is_integral_mul_unit RingHom.isIntegral_of_isIntegral_mul_unit -theorem isIntegral_of_isIntegral_mul_unit {x y : A} {r : R} (hr : algebraMap R A r * y = 1) +theorem IsIntegral.of_mul_unit {x y : A} {r : R} (hr : algebraMap R A r * y = 1) (hx : IsIntegral R (x * y)) : IsIntegral R x := (algebraMap R A).isIntegral_of_isIntegral_mul_unit x y r hr hx -#align is_integral_of_is_integral_mul_unit isIntegral_of_isIntegral_mul_unit +#align is_integral_of_is_integral_mul_unit IsIntegral.of_mul_unit /-- Generalization of `isIntegral_of_mem_closure` bootstrapped up from that lemma -/ theorem isIntegral_of_mem_closure' (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) : ∀ x ∈ Subring.closure G, IsIntegral R x := fun _ hx => - Subring.closure_induction hx hG isIntegral_zero isIntegral_one (fun _ _ => isIntegral_add) - (fun _ => isIntegral_neg) fun _ _ => isIntegral_mul + Subring.closure_induction hx hG isIntegral_zero isIntegral_one (fun _ _ => IsIntegral.add) + (fun _ => IsIntegral.neg) fun _ _ => IsIntegral.mul #align is_integral_of_mem_closure' isIntegral_of_mem_closure' theorem isIntegral_of_mem_closure'' {S : Type*} [CommRing S] {f : R →+* S} (G : Set S) @@ -682,7 +683,7 @@ theorem IsIntegral.det {n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A @[simp] theorem IsIntegral.pow_iff {x : A} {n : ℕ} (hn : 0 < n) : IsIntegral R (x ^ n) ↔ IsIntegral R x := - ⟨isIntegral_of_pow hn, fun hx => IsIntegral.pow hx n⟩ + ⟨IsIntegral.of_pow hn, fun hx => IsIntegral.pow hx n⟩ #align is_integral.pow_iff IsIntegral.pow_iff open TensorProduct @@ -892,13 +893,13 @@ theorem mk'_zero (h : IsIntegral R (0 : B) := isIntegral_zero) : mk' A 0 h = 0 : -- Porting note: Left-hand side does not simplify @[simp] theorem mk'_add (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : - mk' A (x + y) (isIntegral_add hx hy) = mk' A x hx + mk' A y hy := + mk' A (x + y) (IsIntegral.add hx hy) = mk' A x hx + mk' A y hy := algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_add] #align is_integral_closure.mk'_add IsIntegralClosure.mk'_add -- Porting note: Left-hand side does not simplify @[simp] theorem mk'_mul (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : - mk' A (x * y) (isIntegral_mul hx hy) = mk' A x hx * mk' A y hy := + mk' A (x * y) (IsIntegral.mul hx hy) = mk' A x hx * mk' A y hy := algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_mul] #align is_integral_closure.mk'_mul IsIntegralClosure.mk'_mul @@ -1011,13 +1012,13 @@ theorem isIntegral_trans (A_int : Algebra.IsIntegral R A) (x : B) (hx : IsIntegr IsIntegral R x := by rcases hx with ⟨p, pmonic, hp⟩ let S : Set B := ↑(p.map <| algebraMap A B).frange - refine' isIntegral_of_mem_of_FG (adjoin R (S ∪ {x})) _ _ (subset_adjoin <| Or.inr rfl) - refine' fg_trans (FG_adjoin_of_finite (Finset.finite_toSet _) fun x hx => _) _ + refine' IsIntegral.of_mem_of_fg (adjoin R (S ∪ {x})) _ _ (subset_adjoin <| Or.inr rfl) + refine' fg_trans (fg_adjoin_of_finite (Finset.finite_toSet _) fun x hx => _) _ · rw [Finset.mem_coe, frange, Finset.mem_image] at hx rcases hx with ⟨i, _, rfl⟩ rw [coeff_map] - exact map_isIntegral (IsScalarTower.toAlgHom R A B) (A_int _) - · apply FG_adjoin_singleton_of_integral + exact IsIntegral.map (IsScalarTower.toAlgHom R A B) (A_int _) + · apply IsIntegral.fg_adjoin_singleton exact isIntegral_trans_aux _ pmonic hp #align is_integral_trans isIntegral_trans @@ -1047,7 +1048,7 @@ theorem isIntegral_of_surjective (h : Function.Surjective (algebraMap R A)) : /-- If `R → A → B` is an algebra tower with `A → B` injective, then if the entire tower is an integral extension so is `R → A` -/ -theorem isIntegral_tower_bot_of_isIntegral (H : Function.Injective (algebraMap A B)) {x : A} +theorem IsIntegral.tower_bot (H : Function.Injective (algebraMap A B)) {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x := by rcases h with ⟨p, ⟨hp, hp'⟩⟩ refine' ⟨p, ⟨hp, _⟩⟩ @@ -1055,21 +1056,21 @@ theorem isIntegral_tower_bot_of_isIntegral (H : Function.Injective (algebraMap A RingHom.map_zero (algebraMap A B)] at hp' rw [eval₂_eq_eval_map] exact H hp' -#align is_integral_tower_bot_of_is_integral isIntegral_tower_bot_of_isIntegral +#align is_integral_tower_bot_of_is_integral IsIntegral.tower_bot nonrec theorem RingHom.isIntegral_tower_bot_of_isIntegral (hg : Function.Injective g) (hfg : (g.comp f).IsIntegral) : f.IsIntegral := fun x => - @isIntegral_tower_bot_of_isIntegral R S T _ _ _ g.toAlgebra (g.comp f).toAlgebra f.toAlgebra + @IsIntegral.tower_bot R S T _ _ _ g.toAlgebra (g.comp f).toAlgebra f.toAlgebra (@IsScalarTower.of_algebraMap_eq R S T _ _ _ f.toAlgebra g.toAlgebra (g.comp f).toAlgebra (RingHom.comp_apply g f)) hg x (hfg (g x)) #align ring_hom.is_integral_tower_bot_of_is_integral RingHom.isIntegral_tower_bot_of_isIntegral -theorem isIntegral_tower_bot_of_isIntegral_field {R A B : Type*} [CommRing R] [Field A] +theorem IsIntegral.tower_bot_of_field {R A B : Type*} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x := - isIntegral_tower_bot_of_isIntegral (algebraMap A B).injective h -#align is_integral_tower_bot_of_is_integral_field isIntegral_tower_bot_of_isIntegral_field + IsIntegral.tower_bot (algebraMap A B).injective h +#align is_integral_tower_bot_of_is_integral_field IsIntegral.tower_bot_of_field theorem RingHom.isIntegralElem_of_isIntegralElem_comp {x : T} (h : (g.comp f).IsIntegralElem x) : g.IsIntegralElem x := @@ -1098,10 +1099,10 @@ theorem RingHom.isIntegral_quotient_of_isIntegral {I : Ideal S} (hf : f.IsIntegr simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx #align ring_hom.is_integral_quotient_of_is_integral RingHom.isIntegral_quotient_of_isIntegral -theorem isIntegral_quotient_of_isIntegral {I : Ideal A} (hRA : Algebra.IsIntegral R A) : +theorem Algebra.IsIntegral.quotient {I : Ideal A} (hRA : Algebra.IsIntegral R A) : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) := (algebraMap R A).isIntegral_quotient_of_isIntegral hRA -#align is_integral_quotient_of_is_integral isIntegral_quotient_of_isIntegral +#align is_integral_quotient_of_is_integral Algebra.IsIntegral.quotient theorem isIntegral_quotientMap_iff {I : Ideal S} : (Ideal.quotientMap I f le_rfl).IsIntegral ↔ @@ -1161,7 +1162,7 @@ theorem isField_of_isIntegral_of_isField' {R S : Type*} [CommRing R] [CommRing S let A := Algebra.adjoin R ({x} : Set S) haveI : IsNoetherian R A := isNoetherian_of_fg_of_noetherian (Subalgebra.toSubmodule A) - (FG_adjoin_singleton_of_integral x (H x)) + (IsIntegral.fg_adjoin_singleton x (H x)) haveI : Module.Finite R A := Module.IsNoetherian.finite R A obtain ⟨y, hy⟩ := LinearMap.surjective_of_injective diff --git a/Mathlib/RingTheory/IntegrallyClosed.lean b/Mathlib/RingTheory/IntegrallyClosed.lean index df868d407e0204..e1afc13ff9e4ef 100644 --- a/Mathlib/RingTheory/IntegrallyClosed.lean +++ b/Mathlib/RingTheory/IntegrallyClosed.lean @@ -92,7 +92,7 @@ theorem isIntegral_iff {x : K} : IsIntegral R x ↔ ∃ y : R, algebraMap R K y theorem exists_algebraMap_eq_of_isIntegral_pow {x : K} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : ∃ y : R, algebraMap R K y = x := - isIntegral_iff.mp <| isIntegral_of_pow hn hx + isIntegral_iff.mp <| IsIntegral.of_pow hn hx #align is_integrally_closed.exists_algebra_map_eq_of_is_integral_pow IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow theorem exists_algebraMap_eq_of_pow_mem_subalgebra {K : Type*} [CommRing K] [Algebra R K] diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index 09efecea4f3714..ba49f62962b0da 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -137,14 +137,14 @@ theorem isJacobson_of_isIntegral [Algebra R S] (hRS : Algebra.IsIntegral R S) (h · simp [comap_eq_top_iff.1 hP_top] · haveI : Nontrivial (R ⧸ comap (algebraMap R S) P) := Quotient.nontrivial hP_top rw [jacobson_eq_iff_jacobson_quotient_eq_bot] - refine' eq_bot_of_comap_eq_bot (isIntegral_quotient_of_isIntegral hRS) _ + refine' eq_bot_of_comap_eq_bot (Algebra.IsIntegral.quotient hRS) _ rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1 ((isJacobson_iff_prime_eq.1 hR) (comap (algebraMap R S) P) (comap_isPrime _ _)), comap_jacobson] refine' sInf_le_sInf fun J hJ => _ simp only [true_and_iff, Set.mem_image, bot_le, Set.mem_setOf_eq] have : J.IsMaximal := by simpa using hJ - exact exists_ideal_over_maximal_of_isIntegral (isIntegral_quotient_of_isIntegral hRS) J + exact exists_ideal_over_maximal_of_isIntegral (Algebra.IsIntegral.quotient hRS) J (comap_bot_le_of_injective _ algebraMap_quotient_injective) #align ideal.is_jacobson_of_is_integral Ideal.isJacobson_of_isIntegral diff --git a/Mathlib/RingTheory/Localization/Integral.lean b/Mathlib/RingTheory/Localization/Integral.lean index 2b23912eae6e4f..d912e811296213 100644 --- a/Mathlib/RingTheory/Localization/Integral.lean +++ b/Mathlib/RingTheory/Localization/Integral.lean @@ -233,7 +233,7 @@ theorem isIntegral_localization (H : Algebra.IsIntegral R S) : obtain ⟨v, hv⟩ := hu obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩) refine' - @isIntegral_of_isIntegral_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' _ + @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' _ _ · replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv' rw [RingHom.map_mul, RingHom.map_one, ← RingHom.comp_apply _ (algebraMap R Rₘ)] at hv' @@ -392,12 +392,12 @@ theorem isAlgebraic_iff' [Field K] [IsDomain R] [IsDomain S] [Algebra R K] [Alge obtain ⟨a : S, b, ha, rfl⟩ := @div_surjective S _ _ _ _ _ _ x obtain ⟨f, hf₁, hf₂⟩ := h b rw [div_eq_mul_inv] - refine' isIntegral_mul _ _ + refine' IsIntegral.mul _ _ · rw [← isAlgebraic_iff_isIntegral] refine' - _root_.isAlgebraic_of_larger_base_of_injective + IsAlgebraic.of_larger_base_of_injective (NoZeroSMulDivisors.algebraMap_injective R (FractionRing R)) _ - exact isAlgebraic_algebraMap_of_isAlgebraic (h a) + exact IsAlgebraic.algebraMap (h a) · rw [← isAlgebraic_iff_isIntegral] use (f.map (algebraMap R (FractionRing R))).reverse constructor diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean index 0a2728768e0bbe..c88b9a8fc5feb5 100644 --- a/Mathlib/RingTheory/Norm.lean +++ b/Mathlib/RingTheory/Norm.lean @@ -222,7 +222,7 @@ theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_one {x : L} (hx : ¬Is rw [norm_eq_one_of_not_exists_basis] contrapose! hx obtain ⟨s, ⟨b⟩⟩ := hx - refine isIntegral_of_mem_of_FG K⟮x⟯.toSubalgebra ?_ x ?_ + refine IsIntegral.of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_ · exact (Submodule.fg_iff_finiteDimensional _).mpr (of_fintype_basis b) · exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x) #align intermediate_field.adjoin_simple.norm_gen_eq_one IntermediateField.AdjoinSimple.norm_gen_eq_one diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean index 7fe6aa634a1b37..335b19d2eb8579 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean @@ -175,8 +175,8 @@ theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {B : Pow IsIntegral R (z * B.gen ^ n - ∑ x : ℕ in (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) := by refine - isIntegral_sub (isIntegral_mul hzint (IsIntegral.pow hBint _)) - (IsIntegral.sum _ fun i hi => isIntegral_smul _ ?_) + IsIntegral.sub (IsIntegral.mul hzint (IsIntegral.pow hBint _)) + (IsIntegral.sum _ fun i hi => IsIntegral.smul _ ?_) exact adjoin_le_integralClosure hBint (hf _ (aux i hi)).1 obtain ⟨r, hr⟩ := isIntegral_iff.1 (isIntegral_norm K hintsum) use r @@ -351,10 +351,10 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis (∑ x : ℕ in (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1) + ∑ x : ℕ in range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) := by - refine isIntegral_sub (isIntegral_mul hzint (IsIntegral.pow hBint _)) - (isIntegral_add (IsIntegral.sum _ fun k hk => isIntegral_smul _ ?_) + refine IsIntegral.sub (IsIntegral.mul hzint (IsIntegral.pow hBint _)) + (IsIntegral.add (IsIntegral.sum _ fun k hk => IsIntegral.smul _ ?_) (IsIntegral.sum _ fun k _ => - isIntegral_mul (isIntegral_smul _ (IsIntegral.pow hBint _)) (IsIntegral.pow hBint _))) + IsIntegral.mul (IsIntegral.smul _ (IsIntegral.pow hBint _)) (IsIntegral.pow hBint _))) refine adjoin_le_integralClosure hBint (hf _ ?_).1 rw [(minpoly.monic hBint).natDegree_map (algebraMap R L)] rw [add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right] @@ -391,7 +391,7 @@ theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt {B : PowerBa exact hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint - (isIntegral_smul _ hzint) hz hei) + (IsIntegral.smul _ hzint) hz hei) #align mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt end IsIntegral diff --git a/Mathlib/RingTheory/RingHom/Integral.lean b/Mathlib/RingTheory/RingHom/Integral.lean index b26fea87bdddad..6d916fa32df2e1 100644 --- a/Mathlib/RingTheory/RingHom/Integral.lean +++ b/Mathlib/RingTheory/RingHom/Integral.lean @@ -38,7 +38,7 @@ theorem isIntegral_stableUnderBaseChange : StableUnderBaseChange fun f => f.IsIn refine' TensorProduct.induction_on x _ _ _ · apply isIntegral_zero · intro x y; exact IsIntegral.tmul x (h y) - · intro x y hx hy; exact isIntegral_add hx hy + · intro x y hx hy; exact IsIntegral.add hx hy #align ring_hom.is_integral_stable_under_base_change RingHom.isIntegral_stableUnderBaseChange end RingHom diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 138215d0363a63..3679fd6fa56724 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -262,7 +262,7 @@ theorem trace_gen_eq_zero {x : L} (hx : ¬IsIntegral K x) : rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply] contrapose! hx obtain ⟨s, ⟨b⟩⟩ := hx - refine' isIntegral_of_mem_of_FG K⟮x⟯.toSubalgebra _ x _ + refine' IsIntegral.of_mem_of_fg K⟮x⟯.toSubalgebra _ x _ · exact (Submodule.fg_iff_finiteDimensional _).mpr (FiniteDimensional.of_fintype_basis b) · exact subset_adjoin K _ (Set.mem_singleton x) #align intermediate_field.adjoin_simple.trace_gen_eq_zero IntermediateField.AdjoinSimple.trace_gen_eq_zero