Theorem: IsPrincipal_of_IsPrincipal_pow_of_Coprime (FltRegular/NumberTheory/RegularPrimes.lean)

State before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
⊢ Submodule.IsPrincipal I
Tactic:
by_cases Izero : I = 0
State after:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal I

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ Submodule.IsPrincipal I

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ Submodule.IsPrincipal I
Tactic:
rw [← ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_of_ne_zero _)] at hI ⊢
State after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
swap
State after:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
swap
State after:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0

case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1
Tactic:
rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
State after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup A)

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup A)
Tactic:
refine ⟨?_, orderOf_dvd_card⟩
State after:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p

State before:
case neg
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ p
Tactic:
rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow]
State after:
no goals

State before:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal I
Tactic:
rw [Izero]
State after:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal 0

State before:
case pos
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : I = 0
⊢ Submodule.IsPrincipal 0
Tactic:
exact bot_isPrincipal
State after:
no goals

State before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI✝ : Submodule.IsPrincipal (I ^ p)
hI : ClassGroup.mk0 ⟨I ^ p, ⋯⟩ = 1
Izero : ¬I = 0
⊢ I ≠ 0
Tactic:
exact Izero
State after:
no goals

State before:
n p✝ : ℕ
inst✝⁴ : Fact p✝.Prime
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Fintype (ClassGroup A)
p : ℕ
inst✝ : Fact p.Prime
H : p.Coprime (Fintype.card (ClassGroup A))
I : Ideal A
hI : Submodule.IsPrincipal (I ^ p)
Izero : ¬I = 0
⊢ I ^ p ≠ 0
Tactic:
exact pow_ne_zero p Izero
State after:
no goals