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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this : NeZero e := { out := he }
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this : NeZero e := { out := he }
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
letI : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p 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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
letI := Ideal.Quotient.field 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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
have hdim := rank_prime_pow_ramificationIdx _ _ _ hP0 he
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

case neg
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
case neg
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
case neg
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
have hPe := mt (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mp hP
no goals
case neg
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
simp only [finrank_of_infinite_dimensional hP, finrank_of_infinite_dimensional hPe,
  MulZeroClass.mul_zero]
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
haveI := hP
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝³ : NeZero e := { out := he }
this✝² : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝¹ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
haveI := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝³ : NeZero e := { out := he }
this✝² : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝¹ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑(finrank (R ⧸ p) (S ⧸ P ^ e)) = ↑(e * finrank (R ⧸ p) (S ⧸ P))
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝³ : NeZero e := { out := he }
this✝² : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝¹ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
refine' Cardinal.natCast_injective _
no goals
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
he : e ≠ 0
this✝³ : NeZero e := { out := he }
this✝² : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P
this✝¹ : Field (R ⧸ p) := Quotient.field p
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑(finrank (R ⧸ p) (S ⧸ P ^ e)) = ↑(e * finrank (R ⧸ p) (S ⧸ P))
rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]