[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Rat

Mathlib.lean

@@ -2299,6 +2299,7 @@ import Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
 import Mathlib.NumberTheory.Cyclotomic.Basic
 import Mathlib.NumberTheory.Cyclotomic.Discriminant
 import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
+import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.Dioph
 import Mathlib.NumberTheory.DiophantineApproximation
 import Mathlib.NumberTheory.Divisors

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -179,21 +179,43 @@ def equivAdjoin (hx : IsIntegral R x) : AdjoinRoot (minpoly R x) ≃ₐ[R] adjoi
 
 /-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version
 over a field. -/
-@[simps!]
 def _root_.Algebra.adjoin.powerBasis' (hx : IsIntegral R x) :
     PowerBasis R (Algebra.adjoin R ({x} : Set S)) :=
   PowerBasis.map (AdjoinRoot.powerBasis' (minpoly.monic hx)) (minpoly.equivAdjoin hx)
 #align algebra.adjoin.power_basis' Algebra.adjoin.powerBasis'
 
+@[simp]
+theorem _root_.Algebra.adjoin.powerBasis'_dim (hx : IsIntegral R x) :
+  (Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree := rfl
+#align algebra.adjoin.power_basis'_dim Algebra.adjoin.powerBasis'_dim
+
+@[simp]
+theorem _root_.Algebra.adjoin.powerBasis'_gen (hx : IsIntegral R x) :
+    (adjoin.powerBasis' hx).gen = ⟨x, SetLike.mem_coe.1 <| subset_adjoin <| mem_singleton x⟩ := by
+  rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
+    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftHom_root]
+#align algebra.adjoin.power_basis'_gen Algebra.adjoin.powerBasis'_gen
+
 /-- The power basis given by `x` if `B.gen ∈ adjoin R {x}`. -/
-@[simps!]
 noncomputable def _root_.PowerBasis.ofGenMemAdjoin' (B : PowerBasis R S) (hint : IsIntegral R x)
     (hx : B.gen ∈ adjoin R ({x} : Set S)) : PowerBasis R S :=
   (Algebra.adjoin.powerBasis' hint).map <|
     (Subalgebra.equivOfEq _ _ <| PowerBasis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
       Subalgebra.topEquiv
 #align power_basis.of_gen_mem_adjoin' PowerBasis.ofGenMemAdjoin'
 
+@[simp]
+theorem _root_.PowerBasis.ofGenMemAdjoin'_dim (B : PowerBasis R S) (hint : IsIntegral R x)
+    (hx : B.gen ∈ adjoin R ({x} : Set S)) :
+    (B.ofGenMemAdjoin' hint hx).dim = (minpoly R x).natDegree := rfl
+#align power_basis.of_gen_mem_adjoin'_dim PowerBasis.ofGenMemAdjoin'_dim
+
+@[simp]
+theorem _root_.PowerBasis.ofGenMemAdjoin'_gen (B : PowerBasis R S) (hint : IsIntegral R x)
+    (hx : B.gen ∈ adjoin R ({x} : Set S)) :
+    (B.ofGenMemAdjoin' hint hx).gen = x := by
+  simp [PowerBasis.ofGenMemAdjoin']
+#align power_basis.of_gen_mem_adjoin'_gen PowerBasis.ofGenMemAdjoin'_gen
 
 end AdjoinRoot
 

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -0,0 +1,282 @@
+/-
+Copyright (c) 2022 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+
+! This file was ported from Lean 3 source module number_theory.cyclotomic.rat
+! leanprover-community/mathlib commit b353176c24d96c23f0ce1cc63efc3f55019702d9
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.NumberTheory.Cyclotomic.Discriminant
+import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
+
+/-!
+# Ring of integers of `p ^ n`-th cyclotomic fields
+We gather results about cyclotomic extensions of `ℚ`. In particular, we compute the ring of
+integers of a `p ^ n`-th cyclotomic extension of `ℚ`.
+
+## Main results
+* `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`: if `K` is a
+  `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the integral closure of
+  `ℤ` in `K`.
+* `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`: the integral
+  closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is `CyclotomicRing (p ^ k) ℤ ℚ`.
+-/
+
+
+universe u
+
+open Algebra IsCyclotomicExtension Polynomial NumberField
+
+open scoped Cyclotomic NumberField Nat
+
+variable {p : ℕ+} {k : ℕ} {K : Type u} [Field K] [CharZero K] {ζ : K} [hp : Fact (p : ℕ).Prime]
+
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issue #2220
+
+namespace IsCyclotomicExtension.Rat
+
+/-- The discriminant of the power basis given by `ζ - 1`. -/
+theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) :
+    discr ℚ (hζ.subOnePowerBasis ℚ).basis =
+      (-1) ^ ((p ^ (k + 1) : ℕ).totient / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) := by
+  rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (p ^ (k + 1)).pos) hk]
+  exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
+#align is_cyclotomic_extension.rat.discr_prime_pow_ne_two' IsCyclotomicExtension.Rat.discr_prime_pow_ne_two'
+
+theorem discr_odd_prime' [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) :
+    discr ℚ (hζ.subOnePowerBasis ℚ).basis = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) := by
+  rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]
+  exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
+#align is_cyclotomic_extension.rat.discr_odd_prime' IsCyclotomicExtension.Rat.discr_odd_prime'
+
+/-- The discriminant of the power basis given by `ζ - 1`. Beware that in the cases `p ^ k = 1` and
+`p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform
+result. See also `IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'`. -/
+theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
+    discr ℚ (hζ.subOnePowerBasis ℚ).basis =
+      (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1)) := by
+  rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)]
+  exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
+#align is_cyclotomic_extension.rat.discr_prime_pow' IsCyclotomicExtension.Rat.discr_prime_pow'
+
+/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and
+`n : ℕ` such that the discriminant of the power basis given by `ζ - 1` is `u * p ^ n`. Often this is
+enough and less cumbersome to use than `IsCyclotomicExtension.Rat.discr_prime_pow'`. -/
+theorem discr_prime_pow_eq_unit_mul_pow' [IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
+    ∃ (u : ℤˣ) (n : ℕ), discr ℚ (hζ.subOnePowerBasis ℚ).basis = u * p ^ n := by
+  rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]
+  exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)
+#align is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow' IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'
+
+/-- If `K` is a `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the
+integral closure of `ℤ` in `K`. -/
+theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by
+  refine' ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
+  swap
+  · rintro ⟨y, rfl⟩
+    exact
+      IsIntegral.algebraMap
+        (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
+-- Porting note: the following `haveI` was not needed because the locale `cyclotomic` set it
+-- as instances.
+  letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K
+  have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
+  obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ
+  rw [hun] at H
+  replace H := Subalgebra.smul_mem _ H u.inv
+-- Porting note: the proof is slightly different because of coercions.
+  rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul,
+    Units.inv_mul, Int.cast_one, one_mul, PNat.pow_coe, Nat.cast_pow, smul_def, map_pow] at H
+  cases k
+  · haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl
+    have : x ∈ (⊥ : Subalgebra ℚ K) := by
+      rw [singleton_one ℚ K]
+      exact mem_top
+    obtain ⟨y, rfl⟩ := mem_bot.1 this
+    replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
+    obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h
+    rw [← hz, ← IsScalarTower.algebraMap_apply]
+    exact Subalgebra.algebraMap_mem _ _
+  · have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {((p : ℕ) : ℤ)}) := by
+      have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
+      have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
+      rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
+      rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
+        show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
+      haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
+      rw [IsPrimitiveRoot.subOnePowerBasis_gen,
+        map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
+      exact cyclotomic_prime_pow_comp_x_add_one_isEisensteinAt p _
+    refine'
+      adjoin_le _
+        (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at (n := n)
+          (Nat.prime_iff_prime_int.1 hp.out) hint h (by simpa using H) hmin)
+    simp only [Set.singleton_subset_iff, SetLike.mem_coe]
+    exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
+#align is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow
+
+theorem isIntegralClosure_adjoin_singleton_of_prime [hcycl : IsCyclotomicExtension {p} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑p) : IsIntegralClosure (adjoin ℤ ({ζ} : Set K)) ℤ K := by
+  rw [← pow_one p] at hζ hcycl
+  exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ
+#align is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime
+
+/-- The integral closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is
+`CyclotomicRing (p ^ k) ℤ ℚ`. -/
+theorem cyclotomicRing_isIntegralClosure_of_prime_pow :
+    IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ) := by
+  haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
+  have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
+  refine' ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
+-- Porting note: having `.isIntegral_iff` inside the definition of `this` causes an error.
+  · have := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ)
+    obtain ⟨y, rfl⟩ := this.isIntegral_iff.1 h
+    refine' adjoin_mono _ y.2
+    simp only [PNat.pow_coe, Set.singleton_subset_iff, Set.mem_setOf_eq]
+    exact hζ.pow_eq_one
+  · rintro ⟨y, rfl⟩
+    exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _) _)
+#align is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow
+
+theorem cyclotomicRing_isIntegralClosure_of_prime :
+    IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ) := by
+  rw [← pow_one p]
+  exact cyclotomicRing_isIntegralClosure_of_prime_pow
+#align is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime
+
+end IsCyclotomicExtension.Rat
+
+section PowerBasis
+
+open IsCyclotomicExtension.Rat
+
+namespace IsPrimitiveRoot
+
+/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p ^ k`-th root of
+unity and `K` is a `p ^ k`-th cyclotomic extension of `ℚ`. -/
+@[simps!]
+noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers
+    [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
+    adjoin ℤ ({ζ} : Set K) ≃ₐ[ℤ] 𝓞 K :=
+  let _ := isIntegralClosure_adjoin_singleton_of_prime_pow hζ
+  IsIntegralClosure.equiv ℤ (adjoin ℤ ({ζ} : Set K)) K (𝓞 K)
+#align is_primitive_root.adjoin_equiv_ring_of_integers IsPrimitiveRoot.adjoinEquivRingOfIntegers
+
+/-- The ring of integers of a `p ^ k`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/
+instance IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {p ^ k} ℚ K] :
+    IsCyclotomicExtension {p ^ k} ℤ (𝓞 K) :=
+  let _ := (zeta_spec (p ^ k) ℚ K).adjoin_isCyclotomicExtension ℤ
+  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec (p ^ k) ℚ K).adjoinEquivRingOfIntegers
+#align is_cyclotomic_extension.ring_of_integers IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegers
+
+/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k`
+cyclotomic extension of `ℚ`. -/
+noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) :=
+  (Algebra.adjoin.powerBasis' (hζ.isIntegral (p ^ k).pos)).map hζ.adjoinEquivRingOfIntegers
+#align is_primitive_root.integral_power_basis IsPrimitiveRoot.integralPowerBasis
+
+--Porting note: the proof changed because `simp` unfolds too much.
+@[simp]
+theorem integralPowerBasis_gen [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
+    hζ.integralPowerBasis.gen = ⟨ζ, hζ.isIntegral (p ^ k).pos⟩ :=
+  Subtype.ext <| show algebraMap _ K hζ.integralPowerBasis.gen = _ by
+    rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
+    simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
+    rfl
+#align is_primitive_root.integral_power_basis_gen IsPrimitiveRoot.integralPowerBasis_gen
+
+@[simp]
+theorem integralPowerBasis_dim [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : hζ.integralPowerBasis.dim = φ (p ^ k) := by
+  simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ, natDegree_cyclotomic]
+#align is_primitive_root.integral_power_basis_dim IsPrimitiveRoot.integralPowerBasis_dim
+
+/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p`-th root of
+unity and `K` is a `p`-th cyclotomic extension of `ℚ`. -/
+@[simps!]
+noncomputable def _root_.IsPrimitiveRoot.adjoinEquivRingOfIntegers'
+    [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
+    adjoin ℤ ({ζ} : Set K) ≃ₐ[ℤ] 𝓞 K :=
+  @adjoinEquivRingOfIntegers p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
+#align is_primitive_root.adjoin_equiv_ring_of_integers' IsPrimitiveRoot.adjoinEquivRingOfIntegers'
+
+/-- The ring of integers of a `p`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/
+instance _root_.IsCyclotomicExtension.ring_of_integers' [IsCyclotomicExtension {p} ℚ K] :
+    IsCyclotomicExtension {p} ℤ (𝓞 K) :=
+  let _ := (zeta_spec p ℚ K).adjoin_isCyclotomicExtension ℤ
+  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec p ℚ K).adjoinEquivRingOfIntegers'
+#align is_cyclotomic_extension.ring_of_integers' IsCyclotomicExtension.ring_of_integers'
+
+/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p`-th
+cyclotomic extension of `ℚ`. -/
+noncomputable def integralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K]
+    (hζ : IsPrimitiveRoot ζ p) : PowerBasis ℤ (𝓞 K) :=
+  @integralPowerBasis p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
+#align is_primitive_root.integral_power_basis' IsPrimitiveRoot.integralPowerBasis'
+
+@[simp]
+theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
+    hζ.integralPowerBasis'.gen = ⟨ζ, hζ.isIntegral p.pos⟩ :=
+  @integralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
+#align is_primitive_root.integral_power_basis'_gen IsPrimitiveRoot.integralPowerBasis'_gen
+
+@[simp]
+theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
+    hζ.integralPowerBasis'.dim = φ p := by
+  erw [@integralPowerBasis_dim p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]),
+    pow_one]
+#align is_primitive_root.power_basis_int'_dim IsPrimitiveRoot.power_basis_int'_dim
+
+/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic
+extension of `ℚ`. -/
+noncomputable def subOneIntegralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : PowerBasis ℤ (𝓞 K) :=
+  PowerBasis.ofGenMemAdjoin' hζ.integralPowerBasis
+    (isIntegral_of_mem_ringOfIntegers <|
+      Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _))
+    (by
+      simp only [integralPowerBasis_gen]
+      convert Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
+        (Subalgebra.one_mem _)
+-- Porting note: `simp` was able to finish the proof.
+      simp only [Subsemiring.coe_add, Subalgebra.coe_toSubsemiring,
+        OneMemClass.coe_one, sub_add_cancel]
+      exact Subalgebra.sub_mem _ (hζ.isIntegral (by simp)) (Subalgebra.one_mem _))
+#align is_primitive_root.sub_one_integral_power_basis IsPrimitiveRoot.subOneIntegralPowerBasis
+
+@[simp]
+theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {p ^ k} ℚ K]
+    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
+    hζ.subOneIntegralPowerBasis.gen =
+      ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)⟩ :=
+  by simp [subOneIntegralPowerBasis]
+#align is_primitive_root.sub_one_integral_power_basis_gen IsPrimitiveRoot.subOneIntegralPowerBasis_gen
+
+/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p`-th cyclotomic
+extension of `ℚ`. -/
+noncomputable def subOneIntegralPowerBasis' [hcycl : IsCyclotomicExtension {p} ℚ K]
+    (hζ : IsPrimitiveRoot ζ p) : PowerBasis ℤ (𝓞 K) :=
+  @subOneIntegralPowerBasis p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
+#align is_primitive_root.sub_one_integral_power_basis' IsPrimitiveRoot.subOneIntegralPowerBasis'
+
+@[simp]
+theorem subOneIntegralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K]
+    (hζ : IsPrimitiveRoot ζ p) :
+    hζ.subOneIntegralPowerBasis'.gen =
+      ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral p.pos) (Subalgebra.one_mem _)⟩ :=
+  @subOneIntegralPowerBasis_gen p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one])
+#align is_primitive_root.sub_one_integral_power_basis'_gen IsPrimitiveRoot.subOneIntegralPowerBasis'_gen
+
+end IsPrimitiveRoot
+
+end PowerBasis