div — Mathlib

English

Multiplicative congruences preserve division: if w ≡ x and y ≡ z, then w/y ≡ x/z.

Русский

Умножение-деление сохраняются: если w ≡ x и y ≡ z, тогда w/y ≡ x/z.

LaTeX

$$$c\\,w\\,x \\rightarrow c\\,y\\,z \\Rightarrow c\\left(\\dfrac{w}{y}\\right)\\left(\\dfrac{x}{z}\\right)$$$

Lean4

/-- Multiplicative congruence relations preserve division. -/
@[to_additive /-- Additive congruence relations preserve subtraction. -/
    ]
protected theorem div : ∀ {w x y z}, c w x → c y z → c (w / y) (x / z) :=
  @fun w x y z h1 h2 => by simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)

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