coe_primesOverFinset — Mathlib

English

Equality of the finite primes over a maximal ideal after a base change.

Русский

Согласование множеств простых надмаксимаций после базового перехода.

LaTeX

$$primesOverFinset p B = primesOver p B$$

Lean4

theorem coe_primesOverFinset : primesOverFinset p B = primesOver p B := by
  classical
  ext P
  rw [primesOverFinset, factors_eq_normalizedFactors, Finset.mem_coe, Multiset.mem_toFinset]
  exact
    (P.mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hpb)).trans <|
      Iff.intro (fun ⟨hPp, h⟩ => ⟨hPp, ⟨hpm.eq_of_le (comap_ne_top _ hPp.ne_top) (le_comap_of_map_le h)⟩⟩)
        (fun ⟨hPp, h⟩ => ⟨hPp, map_le_of_le_comap h.1.le⟩)

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