mul_right_le_iff — Mathlib

English

For Dedekind domain A and nonzero J, J·I ≤ J·I' iff I ≤ I'.

Русский

Для Дедекинд домена A и ненулевого J верно: J·I ≤ J·I' тогда и только тогда, когда I ≤ I'.

LaTeX

$$$$\\forall I,I',\\; J\\neq 0:\\; J\\cdot I \\le J\\cdot I' \\iff I \\le I'.$$$$

Lean4

theorem mul_right_le_iff [IsDedekindDomain A] {J : FractionalIdeal A⁰ K} (hJ : J ≠ 0) :
    ∀ {I I'}, I * J ≤ I' * J ↔ I ≤ I' := by
  intro I I'
  constructor
  · intro h
    convert mul_right_mono J⁻¹ h <;> dsimp only <;> rw [mul_assoc, FractionalIdeal.mul_inv_cancel hJ, mul_one]
  · exact fun h => mul_right_mono J h

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