emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso

English

For primes p dividing m and a divisor orderIso d, the emultiplicity of p in m equals the emultiplicity of its image in n.

Русский

Для простого p, делящего m, и отображения-изоморфизма делителей d, эмполифичность p по m равна эмполифичности образа в n.

LaTeX

$$emultiplicity p m = emultiplicity (d ⟨p, dvd_of_mem_normalizedFactors hp⟩).val n$$

Lean4

theorem emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso {m p : Associates M} {n : Associates N}
    (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
    emultiplicity p m ≤ emultiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n :=
  by
  by_cases hn : n = 0
  · simp [hn]
  by_cases hm : m = 0
  · simp [hm] at hp
  rw [FiniteMultiplicity.of_prime_left (prime_of_normalized_factor p hp) hm |>.emultiplicity_eq_multiplicity, ←
    pow_dvd_iff_le_emultiplicity]
  apply pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd ..)

Похожие утверждения