R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K :=
  FractionalIdeal.mapEquiv (FractionRing.algEquiv A K)
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ ↑h.toEquiv x ≠ ⊥ → ↑h.toEquiv x * (↑h.toEquiv x)⁻¹ = 1
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
refine h.toEquiv.forall_congr (fun {x} => ?_)
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → ↑h.toEquiv (x * x⁻¹) = ↑h.toEquiv 1 ↔ ↑h.toEquiv x ≠ ⊥ → ↑h.toEquiv x * (↑h.toEquiv x)⁻¹ = 1
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ ↑h.toEquiv x ≠ ⊥ → ↑h.toEquiv x * (↑h.toEquiv x)⁻¹ = 1
rw [← h.toEquiv.apply_eq_iff_eq]
no goals
R : Type ?u.96084
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → ↑h.toEquiv (x * x⁻¹) = ↑h.toEquiv 1 ↔ ↑h.toEquiv x ≠ ⊥ → ↑h.toEquiv x * (↑h.toEquiv x)⁻¹ = 1
simp [IsDedekindDomainInv]