R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this : NeZero e := { out := he }
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
letI : NeZero e := ⟨he⟩
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ 0) } = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this : NeZero e := { out := he }
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
have := rank_pow_quot f p P hP0 0 (Nat.zero_le e)
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) { x // x ∈ ⊤ } = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ 0) } = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
rw [pow_zero, Nat.sub_zero, Ideal.one_eq_top, Ideal.map_top] at this
no goals
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) { x // x ∈ ⊤ } = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
exact (rank_top (R ⧸ p) _).symm.trans this