R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
⊢ I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
conv_lhs => congr; rw [eq_spanSingleton_of_principal I]
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
⊢ generator ↑I ≠ 0
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
⊢ spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
rw [spanSingleton_mul_spanSingleton, mul_inv_cancel, spanSingleton_one]
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ False
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
⊢ generator ↑I ≠ 0
intro generator_I_eq_zero
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ False
apply h
no goals
R : Type ?u.65551
A : Type ?u.65554
K : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : Field K
inst✝¹¹ : IsDomain A
R₁✝ : Type ?u.65752
inst✝¹⁰ : CommRing R₁✝
inst✝⁹ : IsDomain R₁✝
inst✝⁸ : Algebra R₁✝ K
inst✝⁷ : IsFractionRing R₁✝ K
I✝ J : FractionalIdeal R₁✝⁰ K
K' : Type ?u.66565
inst✝⁶ : Field K'
inst✝⁵ : Algebra R₁✝ K'
inst✝⁴ : IsFractionRing R₁✝ K'
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : IsPrincipal ↑I
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0
rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]