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

State before:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsRegularNumber 2
Tactic:
rw [IsRegularNumber]
State after:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Coprime 2 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))))

State before:
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Coprime 2 (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))))
Tactic:
convert coprime_one_right _
State after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))) = 1

State before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))) = 1
Tactic:
dsimp
State after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField 2 ℚ))) = 1

State before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Fintype.card (ClassGroup (𝓞 (CyclotomicField 2 ℚ))) = 1
Tactic:
apply (card_classGroup_eq_one_iff (R := 𝓞 (CyclotomicField (⟨2, two_pos⟩ : ℕ+) ℚ))).2
State after:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))

State before:
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))
Tactic:
infer_instance
State after:
no goals