instance Module.IsTorsionFree.of_noZeroSMulDivisors {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B] : IsTorsionFree A B

@[reducible, inline]

noncomputable abbrev reducedMinpoly (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [Algebra A B] (α : B) : Polynomial (IsLocalRing.ResidueField A)

theorem minpoly_irreducible_of_dvr (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] (α : B) : Irreducible (minpoly A α)

theorem residue_separable_of_irred_sep_reduction (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] (α : B) (hα : A[α] = ⊤) (hirred : Irreducible (reducedMinpoly A B α)) (hsep : (reducedMinpoly A B α).Separable) : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem finrank_eq_of_irred_reduction (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (α : B) (hα : A[α] = ⊤) (hirred : Irreducible (reducedMinpoly A B α)) : Module.finrank A B = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem reduced_minpoly_separable_of_separable_residue (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (α : B) (hα : A[α] = ⊤) (hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (hdeg : Module.finrank A B = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) : (reducedMinpoly A B α).Separable

theorem reduced_minpoly_irreducible (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] (α : B) (hsep : (reducedMinpoly A B α).Separable) : Irreducible (reducedMinpoly A B α)

theorem cor_10_15_forward (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] [IsUnramifiedDVRExtension A B] [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] : ∃ (α : B), A[α] = ⊤ ∧ (reducedMinpoly A B α).Separable

theorem cor_10_15_reverse (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (α : B) (hα : A[α] = ⊤) (hsep_red : (reducedMinpoly A B α).Separable) : IsUnramifiedDVRExtension A B

theorem cor_10_15 (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] : IsUnramifiedDVRExtension A B ↔ ∃ (α : B), A[α] = ⊤ ∧ (reducedMinpoly A B α).Separable

theorem minpoly_reduction_separable (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B] {n : ℕ} {ζ : B} (hζ_int : IsIntegral A ζ) (hζ : ζ ^ n = 1) (hn : ↑n ≠ 0) : (Polynomial.map (IsLocalRing.residue A) (minpoly A ζ)).Separable

theorem cyclotomic_extension_unramified (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {n : ℕ} {ζ : B} (hprim : IsPrimitiveRoot ζ n) (hn : ↑n ≠ 0) (hgen : A[ζ] = ⊤) : IsUnramifiedDVRExtension A B

theorem cor_10_16_of_adjoin (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {n : ℕ} {ζ : B} (hprim : IsPrimitiveRoot ζ n) (hcoprime : n.Coprime (ringChar (IsLocalRing.ResidueField A))) (hgen : A[ζ] = ⊤) : IsUnramifiedDVRExtension A B