change Ideal.map (galRestrict A K L B σ : B →+* B) _ = _ at hβ
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map ((galRestrict A K L B) σ) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra A L
inst✝⁵ : Algebra A K
inst✝⁴ : Algebra B L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsFractionRing A K
inst✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}