mulZeroOneClass — Mathlib

English

For a ≠ 0, the relation a · S ≤ T is equivalent to S ≤ a⁻¹ · T, and similarly the corresponding Iff statements hold for all S,T.

Русский

Для a ≠ 0 верно: a · S ≤ T эквивалентно S ≤ a⁻¹ · T, и такие же эквивалентности справедливы для всех S,T.

LaTeX

$$$\forall a \neq 0,\ S,T:\text{AddSubmonoid } A:\ a\cdot S \le T \iff S \le a^{-1}\cdot T$.$$

Lean4

instance mulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass (ULift α) :=
  Equiv.ulift.injective.mulZeroOneClass _ rfl rfl (by intros; rfl)

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