Theorem: Ideal.map_spanIntNorm (FltRegular/NumberTheory/IdealNorm.lean)

State before:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝² : IsIntegrallyClosed S
inst✝¹ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ map f (spanIntNorm R I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Tactic:
rw [spanIntNorm, map_span, Set.image_image]
State after:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝² : IsIntegrallyClosed S
inst✝¹ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => f ((Algebra.intNorm R S) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

State before:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝² : IsIntegrallyClosed S
inst✝¹ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => f ((Algebra.intNorm R S) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Tactic:
rfl
State after:
no goals