le_iff_dvd

Mathlib.RingTheory.Valuation.Integers

URI: https://scilib.ai/kg/mathlib#Valuation.Integers.le_iff_dvd

English

Membership under comap corresponds to membership after applying the ring homomorphism.

Русский

Членство в A.comap f эквивалентно членству после применения кольцевого гомоморфизма f.

LaTeX

$$$ x \in A^{\mathrm{comap} f} \iff f(x) \in A. $$$

Lean4

theorem le_iff_dvd (hv : Integers v O) {x y : O} : v (algebraMap O F x) ≤ v (algebraMap O F y) ↔ y ∣ x :=
  ⟨hv.dvd_of_le, hv.le_of_dvd⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru