Module

Index.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Index

24 declarations indexed from sourceView source ↗

Module documentation

Index calculus for the tame Abhyankar frontier

The geometric input of tame Abhyankar is a source theorem bounding the ramification index after base change by e / gcd e e'. This file proves the arithmetic consequences of that bound. It deliberately does not assert the geometric bound itself.

Imports3

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Basic
Mathlib.Data.Nat.Factorization.Basic
Mathlib.Data.Nat.Prime.Basic

Imported by4

def

AbhyankarIndexBound

L26 ↗

TameAbhyankar.AbhyankarIndexBound

Documentation

The index bound supplied by the geometric tame-base-change step: the ramification index after base change divides e / gcd e e'.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

def AbhyankarIndexBound (e baseChangeRamificationIndex newRamificationIndex : ℕ) :
    Prop

theorem

div_gcd_eq_one_of_dvd

L30 ↗

TameAbhyankar.div_gcd_eq_one_of_dvd

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem div_gcd_eq_one_of_dvd {e baseChangeRamificationIndex : ℕ}
    (he : 0 < e) (hdiv : e ∣ baseChangeRamificationIndex) :
    e / Nat.gcd e baseChangeRamificationIndex = 1

theorem

lcm_div_right_eq_div_gcd

L38 ↗

TameAbhyankar.lcm_div_right_eq_div_gcd

Documentation

Dividing the lcm by the right input removes exactly the common gcd from the left input. This is the arithmetic shape of the value-group computation behind tame Abhyankar.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem lcm_div_right_eq_div_gcd {e baseChangeRamificationIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex) :
    Nat.lcm e baseChangeRamificationIndex / baseChangeRamificationIndex =
      e / Nat.gcd e baseChangeRamificationIndex

theorem

abhyankarIndexBound_of_mul_eq_lcm

L76 ↗

TameAbhyankar.abhyankarIndexBound_of_mul_eq_lcm

Documentation

If a tower/value-group computation identifies baseChangeRamificationIndex * newRamificationIndex with the lcm of the two lower ramification indices, the tame Abhyankar index bound follows by pure arithmetic.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem abhyankarIndexBound_of_mul_eq_lcm
    {e baseChangeRamificationIndex newRamificationIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        Nat.lcm e baseChangeRamificationIndex) :
    AbhyankarIndexBound e baseChangeRamificationIndex
      newRamificationIndex

theorem

abhyankarIndexBound_of_mul_dvd_lcm

L96 ↗

TameAbhyankar.abhyankarIndexBound_of_mul_dvd_lcm

Documentation

Divisibility form of the lcm source: it is enough for baseChangeRamificationIndex * newRamificationIndex to divide the lcm of the two lower ramification indices.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem abhyankarIndexBound_of_mul_dvd_lcm
    {e baseChangeRamificationIndex newRamificationIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex)
    (hprod_dvd :
      baseChangeRamificationIndex * newRamificationIndex ∣
        Nat.lcm e baseChangeRamificationIndex) :
    AbhyankarIndexBound e baseChangeRamificationIndex
      newRamificationIndex

theorem

div_gcd_dvd_of_lcm_dvd_mul_left

L112 ↗

TameAbhyankar.div_gcd_dvd_of_lcm_dvd_mul_left

Documentation

If the lcm of two value steps divides a * c, the primitive part of the second step after removing the common gcd with a divides c.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem div_gcd_dvd_of_lcm_dvd_mul_left {a b c : ℕ}
    (ha : 0 < a) (hdiv : Nat.lcm a b ∣ a * c) :
    b / Nat.gcd a b ∣ c

theorem

div_gcd_dvd_right_of_mul_eq_mul

L139 ↗

TameAbhyankar.div_gcd_dvd_right_of_mul_eq_mul

Documentation

In a ramification square product, the primitive part of the left lower index divides the right upper branch. This is the unavoidable arithmetic content of the square before the tame/value-group input removes the remaining common quotient.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem div_gcd_dvd_right_of_mul_eq_mul
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex) :
    e / Nat.gcd e baseChangeRamificationIndex ∣
      newRamificationIndex

theorem

div_gcd_dvd_left_of_mul_eq_mul

L187 ↗

TameAbhyankar.div_gcd_dvd_left_of_mul_eq_mul

Documentation

Symmetric primitive-part divisibility for the other upper branch of a ramification square product.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem div_gcd_dvd_left_of_mul_eq_mul
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex) :
    baseChangeRamificationIndex / Nat.gcd e baseChangeRamificationIndex ∣
      leftBaseChangedIndex

theorem

exists_commonPrimitiveQuotient_of_mul_eq_mul

L211 ↗

TameAbhyankar.exists_commonPrimitiveQuotient_of_mul_eq_mul

Documentation

A ramification square product factors both upper branches through the primitive lower ramification indices and a single common quotient. The tame Abhyankar value-group step is precisely the source that must force this common quotient to be 1.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_commonPrimitiveQuotient_of_mul_eq_mul
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex) :
    ∃ commonQuotient,
      newRamificationIndex =
          (e / Nat.gcd e baseChangeRamificationIndex) *
            commonQuotient ∧
        leftBaseChangedIndex =
          (baseChangeRamificationIndex /
            Nat.gcd e baseChangeRamificationIndex) *
              commonQuotient

theorem

right_eq_div_gcd_iff_left_eq_div_gcd_of_mul_eq_mul

L298 ↗

TameAbhyankar.right_eq_div_gcd_iff_left_eq_div_gcd_of_mul_eq_mul

Documentation

In a ramification square product, the two upper branches are primitive at the same time: both are obtained from their primitive lower parts by the same common quotient. This isolates the arithmetic point that forcing the common quotient to be 1 can be checked on either upper branch.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem right_eq_div_gcd_iff_left_eq_div_gcd_of_mul_eq_mul
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : Nat}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex) :
    Iff
      (newRamificationIndex =
        e / Nat.gcd e baseChangeRamificationIndex)
      (leftBaseChangedIndex =
        baseChangeRamificationIndex /
          Nat.gcd e baseChangeRamificationIndex)

theorem

right_ne_div_gcd_iff_left_ne_div_gcd_of_mul_eq_mul

L356 ↗

TameAbhyankar.right_ne_div_gcd_iff_left_ne_div_gcd_of_mul_eq_mul

Documentation

Contrapositive form of right_eq_div_gcd_iff_left_eq_div_gcd_of_mul_eq_mul, useful for moving a non-primitive obstruction between the two upper branches without introducing a new branch-coprimality assumption.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem right_ne_div_gcd_iff_left_ne_div_gcd_of_mul_eq_mul
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : Nat}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex) :
    Iff
      (Not (newRamificationIndex =
        e / Nat.gcd e baseChangeRamificationIndex))
      (Not (leftBaseChangedIndex =
        baseChangeRamificationIndex /
          Nat.gcd e baseChangeRamificationIndex))

theorem

exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_right_le

L380 ↗

TameAbhyankar.exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_right_le

Documentation

If the right upper branch of a ramification square is bounded by the left lower index, then the common primitive quotient is bounded by the lower gcd.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_right_le
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_le : newRamificationIndex ≤ e) :
    ∃ commonQuotient,
      newRamificationIndex =
          (e / Nat.gcd e baseChangeRamificationIndex) *
            commonQuotient ∧
        leftBaseChangedIndex =
          (baseChangeRamificationIndex /
            Nat.gcd e baseChangeRamificationIndex) *
              commonQuotient ∧
        commonQuotient ≤ Nat.gcd e baseChangeRamificationIndex

theorem

exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_left_le

L425 ↗

TameAbhyankar.exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_left_le

Documentation

Symmetric bound for the common primitive quotient, using the left upper branch bound by the right lower index.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_commonPrimitiveQuotient_le_gcd_of_mul_eq_mul_of_left_le
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hleft_le : leftBaseChangedIndex ≤ baseChangeRamificationIndex) :
    ∃ commonQuotient,
      newRamificationIndex =
          (e / Nat.gcd e baseChangeRamificationIndex) *
            commonQuotient ∧
        leftBaseChangedIndex =
          (baseChangeRamificationIndex /
            Nat.gcd e baseChangeRamificationIndex) *
              commonQuotient ∧
        commonQuotient ≤ Nat.gcd e baseChangeRamificationIndex

theorem

exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_right_le_of_ne

L470 ↗

TameAbhyankar.exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_right_le_of_ne

Documentation

A non-primitive right upper branch exposes a common prime divisor of the two upper branches.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_right_le_of_ne
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_le : newRamificationIndex ≤ e)
    (hnew_ne :
      newRamificationIndex ≠ e / Nat.gcd e baseChangeRamificationIndex) :
    ∃ commonQuotient,
      commonQuotient ≤ Nat.gcd e baseChangeRamificationIndex ∧
        newRamificationIndex =
          (e / Nat.gcd e baseChangeRamificationIndex) * commonQuotient ∧
        leftBaseChangedIndex =
          (baseChangeRamificationIndex /
            Nat.gcd e baseChangeRamificationIndex) * commonQuotient ∧
        ∃ p, Nat.Prime p ∧ p ∣ commonQuotient ∧
          p ∣ newRamificationIndex ∧ p ∣ leftBaseChangedIndex

theorem

exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_left_le_of_ne

L506 ↗

TameAbhyankar.exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_left_le_of_ne

Documentation

Symmetric prime obstruction extracted from the left upper branch.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_prime_commonPrimitiveObstruction_of_mul_eq_mul_of_left_le_of_ne
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hleft_le : leftBaseChangedIndex ≤ baseChangeRamificationIndex)
    (hleft_ne :
      leftBaseChangedIndex ≠
        baseChangeRamificationIndex /
          Nat.gcd e baseChangeRamificationIndex) :
    ∃ commonQuotient,
      commonQuotient ≤ Nat.gcd e baseChangeRamificationIndex ∧
        newRamificationIndex =
          (e / Nat.gcd e baseChangeRamificationIndex) *
            commonQuotient ∧
        leftBaseChangedIndex =
          (baseChangeRamificationIndex /
            Nat.gcd e baseChangeRamificationIndex) *
              commonQuotient ∧
        ∃ p, Nat.Prime p ∧ p ∣ commonQuotient ∧
          p ∣ newRamificationIndex ∧ p ∣ leftBaseChangedIndex

theorem

left_eq_div_gcd_of_mul_eq_mul_of_left_le_of_coprime

L546 ↗

TameAbhyankar.left_eq_div_gcd_of_mul_eq_mul_of_left_le_of_coprime

Documentation

Symmetric obstruction elimination for the left upper branch.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem left_eq_div_gcd_of_mul_eq_mul_of_left_le_of_coprime
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (he : 0 < e) (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hleft_le : leftBaseChangedIndex ≤ baseChangeRamificationIndex)
    (hcop : Nat.Coprime newRamificationIndex leftBaseChangedIndex) :
    leftBaseChangedIndex =
      baseChangeRamificationIndex /
        Nat.gcd e baseChangeRamificationIndex

theorem

exists_commonQuotient_of_mul_eq_mul_of_dvd_of_dvd

L569 ↗

TameAbhyankar.exists_commonQuotient_of_mul_eq_mul_of_dvd_of_dvd

Documentation

A split ramification square with divisibility on both upper branches has a common quotient. This isolates the arithmetic datum still left after the source square and branch divisibilities have been constructed.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem exists_commonQuotient_of_mul_eq_mul_of_dvd_of_dvd
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (hnew : 0 < newRamificationIndex)
    (hleftBaseChanged : 0 < leftBaseChangedIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_dvd : newRamificationIndex ∣ e)
    (hleftBaseChanged_dvd :
      leftBaseChangedIndex ∣ baseChangeRamificationIndex) :
    ∃ commonQuotient,
      e = newRamificationIndex * commonQuotient ∧
        baseChangeRamificationIndex =
          leftBaseChangedIndex * commonQuotient

theorem

quotient_eq_of_mul_eq_mul_of_dvd_of_dvd

L618 ↗

TameAbhyankar.quotient_eq_of_mul_eq_mul_of_dvd_of_dvd

Documentation

Quotient form of exists_commonQuotient_of_mul_eq_mul_of_dvd_of_dvd: after cancelling the two upper branch indices, the two lower ramification indices leave the same quotient.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem quotient_eq_of_mul_eq_mul_of_dvd_of_dvd
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (hnew : 0 < newRamificationIndex)
    (hleftBaseChanged : 0 < leftBaseChangedIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_dvd : newRamificationIndex ∣ e)
    (hleftBaseChanged_dvd :
      leftBaseChangedIndex ∣ baseChangeRamificationIndex) :
    e / newRamificationIndex =
      baseChangeRamificationIndex / leftBaseChangedIndex

theorem

mul_eq_lcm_of_mul_eq_mul_of_dvd_of_dvd_of_coprime

L650 ↗

TameAbhyankar.mul_eq_lcm_of_mul_eq_mul_of_dvd_of_dvd_of_coprime

Documentation

Reconstruct the lower-index lcm from a split ramification square whose upper branches divide their respective lower branches and are coprime.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem mul_eq_lcm_of_mul_eq_mul_of_dvd_of_dvd_of_coprime
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (hnew : 0 < newRamificationIndex)
    (hleftBaseChanged : 0 < leftBaseChangedIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_dvd : newRamificationIndex ∣ e)
    (hleftBaseChanged_dvd :
      leftBaseChangedIndex ∣ baseChangeRamificationIndex)
    (hcop : Nat.Coprime newRamificationIndex leftBaseChangedIndex) :
    baseChangeRamificationIndex * newRamificationIndex =
      Nat.lcm e baseChangeRamificationIndex

theorem

abhyankarIndexBound_of_mul_eq_mul_of_dvd_of_dvd_of_coprime

L693 ↗

TameAbhyankar.abhyankarIndexBound_of_mul_eq_mul_of_dvd_of_dvd_of_coprime

Documentation

Split-product source form of the tame Abhyankar index bound.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem abhyankarIndexBound_of_mul_eq_mul_of_dvd_of_dvd_of_coprime
    {e baseChangeRamificationIndex newRamificationIndex
      leftBaseChangedIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex)
    (hnew : 0 < newRamificationIndex)
    (hleftBaseChanged : 0 < leftBaseChangedIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        e * leftBaseChangedIndex)
    (hnew_dvd : newRamificationIndex ∣ e)
    (hleftBaseChanged_dvd :
      leftBaseChangedIndex ∣ baseChangeRamificationIndex)
    (hcop : Nat.Coprime newRamificationIndex leftBaseChangedIndex) :
    AbhyankarIndexBound e baseChangeRamificationIndex
      newRamificationIndex

theorem

eq_one_of_abhyankarIndexBound_of_dvd

L712 ↗

TameAbhyankar.eq_one_of_abhyankarIndexBound_of_dvd

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem eq_one_of_abhyankarIndexBound_of_dvd
    {e baseChangeRamificationIndex newRamificationIndex : ℕ}
    (he : 0 < e)
    (hbound :
      AbhyankarIndexBound e baseChangeRamificationIndex newRamificationIndex)
    (hdiv : e ∣ baseChangeRamificationIndex) :
    newRamificationIndex = 1

theorem

eq_one_of_dvd_of_dvd_of_coprime

L725 ↗

TameAbhyankar.eq_one_of_dvd_of_dvd_of_coprime

Documentation

If newRamificationIndex divides a ramification index which itself divides a coprime base-change ramification index, then the new index is one.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem eq_one_of_dvd_of_dvd_of_coprime
    {e baseChangeRamificationIndex newRamificationIndex : ℕ}
    (hnew_dvd : newRamificationIndex ∣ e)
    (hdiv : e ∣ baseChangeRamificationIndex)
    (hcop : Nat.Coprime e baseChangeRamificationIndex) :
    newRamificationIndex = 1

theorem

eq_one_of_mul_eq_lcm_of_dvd

L737 ↗

TameAbhyankar.eq_one_of_mul_eq_lcm_of_dvd

Documentation

Direct lcm-product absorption: if the base-change ramification index absorbs the lower ramification index, then the new ramification index is one.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem eq_one_of_mul_eq_lcm_of_dvd
    {e baseChangeRamificationIndex newRamificationIndex : ℕ}
    (hbase : 0 < baseChangeRamificationIndex)
    (hprod :
      baseChangeRamificationIndex * newRamificationIndex =
        Nat.lcm e baseChangeRamificationIndex)
    (hdiv : e ∣ baseChangeRamificationIndex) :
    newRamificationIndex = 1

theorem

abhyankarIndexBound_iff_dvd

L752 ↗

TameAbhyankar.abhyankarIndexBound_iff_dvd

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace TameAbhyankar

Lean source · statement

theorem abhyankarIndexBound_iff_dvd
    (e baseChangeRamificationIndex newRamificationIndex : ℕ) :
    AbhyankarIndexBound e baseChangeRamificationIndex newRamificationIndex ↔
      newRamificationIndex ∣ e / Nat.gcd e baseChangeRamificationIndex

Module documentation

Index calculus for the tame Abhyankar frontier

Declarations