Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime' (FltRegular/CaseII/AuxLemmas.lean)

State before:
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
⊢ (↑I).IsPrincipal
Tactic:
by_cases Izero : I = 0
State after:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ (↑I).IsPrincipal

case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : ¬I = 0
⊢ (↑I).IsPrincipal

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : ¬I = 0
⊢ (↑I).IsPrincipal
Tactic:
rw [← Ne, ← isUnit_iff_ne_zero] at Izero
State after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑I).IsPrincipal

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑I).IsPrincipal
Tactic:
show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K)
State after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑Izero.unit').IsPrincipal

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑Izero.unit').IsPrincipal
Tactic:
rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
State after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p ∧ orderOf (ClassGroup.mk Izero.unit') ∣ Fintype.card (ClassGroup A)

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p ∧ orderOf (ClassGroup.mk Izero.unit') ∣ Fintype.card (ClassGroup A)
Tactic:
refine ⟨?_, orderOf_dvd_card⟩
State after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p
Tactic:
rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff]
State after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑(Izero.unit' ^ p)).IsPrincipal

State before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑(Izero.unit' ^ p)).IsPrincipal
Tactic:
simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI]
State after:
no goals

State before:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ (↑I).IsPrincipal
Tactic:
rw [Izero, FractionalIdeal.coe_zero]
State after:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ ⊥.IsPrincipal

State before:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ ⊥.IsPrincipal
Tactic:
exact bot_isPrincipal
State after:
no goals